Verified Commit adc28e0f authored by Tej Chajed's avatar Tej Chajed

Rename top-level logical path to fit Iris style

parent fc5c9162
......@@ -9,7 +9,7 @@ using Ltac2, providing support for Gallina names in Iris intro patterns on Coq
Simply require this file before using the feature in the proof mode:
From IrisStringIdent Require ltac2_string_ident.
From iris_string_ident Require ltac2_string_ident.
From iris.proofmode Require Import tactics intro_patterns.
Lemma sep_demo {PROP: sbi} (P1: PROP) (P2 P3: Prop) (Himpl: P2 -> P3) :
-Q theories IrisStringIdent
-Q theories iris_string_ident
......@@ -23,5 +23,5 @@ install: [make "install"]
tags: [
"category:Miscellaneous/Coq Extensions"
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