Commit 6382ac89 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'update-string-ident-use' into 'master'

Correct use of iris-string-ident

See merge request iris/examples!33
parents 1ad7fe2f b80f15df
......@@ -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