Correct use of iris-string-ident

Using plain `Require` is unsupported, as discussed in
iris/string-ident!3.
parent 1ad7fe2f
......@@ -4,7 +4,7 @@ From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris_examples.logatom.rdcss Require Import spec.
From iris_string_ident Require ltac2_string_ident.
From iris_string_ident Require Import ltac2_string_ident..
Import uPred bi List Decidable.
Set Default Proof Using "Type".
......
......@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation par.
From iris_examples.logatom.snapshot Require Import spec.
From iris_string_ident Require ltac2_string_ident.
From iris_string_ident Require Import ltac2_string_ident..
Set Default Proof Using "Type".
(** Specifying snapshots with histories
......
......@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris_string_ident Require ltac2_string_ident.
From iris_string_ident Require Import ltac2_string_ident..
Set Default Proof Using "Type".
Fixpoint val_of_list (vs : list (val * val)) : val :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment