Skip to content
Snippets Groups Projects
Verified Commit 090cdbf9 authored by Tej Chajed's avatar Tej Chajed
Browse files

Reword directing to iris/string-ident

parent 6a9afe85
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 3 deletions
CHANGELOG.md
+ 3
− 3
View file @ 090cdbf9
...@@ -103,9 +103,9 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -103,9 +103,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
+ `singleton_included_exclusive` → `singleton_included_exclusive_l` + `singleton_included_exclusive` → `singleton_included_exclusive_l`
* The proof mode now supports names for pure facts in intro patterns. Support * The proof mode now supports names for pure facts in intro patterns. Support
requires implementing `string_to_ident`. Without this tactic such patterns requires implementing `string_to_ident`. Without this tactic such patterns
will fail. We provide one implementation at will fail. We provide one implementation using Ltac2 which works with Coq 8.11
https://gitlab.mpi-sws.org/iris/string-ident using Ltac2 which works with Coq and can be installed with opam; see
8.11 and can be installed with opam (see the README for details). [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
**Changes in heap_lang:** **Changes in heap_lang:**
......
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