Commit 51a9d973 authored by Hugo Herbelin's avatar Hugo Herbelin

The Tactic Notation entry simple_intropattern now binds to Coq simple_intropattern.

Formerly it was bound to Coq entry intropattern.

See Coq PR#10239
parent 5c07c3be
......@@ -453,8 +453,8 @@ In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
"iIntro (constr)", last call failed.
Tactic failure: iIntro: "HP" not fresh.
The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed.
In nested Ltac calls to "iIntros ( (simple_intropattern) )",
"iIntro ( (simple_intropattern) )" and "intros x", last call failed.
x is already used.
"iSplitL_one_of_many"
: string
......
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