Commit db57a33e authored by Ralf Jung's avatar Ralf Jung

Make Ltac helper function local

parent b39f5a52
...@@ -36,11 +36,11 @@ Ltac call to "done" failed. ...@@ -36,11 +36,11 @@ Ltac call to "done" failed.
No applicable tactic. No applicable tactic.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"iElaborateSelPat_go", last call failed. "<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found. Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"iElaborateSelPat_go", last call failed. "<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found. Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)", In nested Ltac calls to "iSpecialize (open_constr)",
......
...@@ -140,7 +140,7 @@ Local Inductive esel_pat := ...@@ -140,7 +140,7 @@ Local Inductive esel_pat :=
| ESelPure | ESelPure
| ESelIdent : bool ident esel_pat. | ESelIdent : bool ident esel_pat.
Ltac iElaborateSelPat_go pat Δ Hs := Local Ltac iElaborateSelPat_go pat Δ Hs :=
lazymatch pat with lazymatch pat with
| [] => eval cbv in Hs | [] => eval cbv in Hs
| SelPure :: ?pat => iElaborateSelPat_go pat Δ (ESelPure :: Hs) | SelPure :: ?pat => iElaborateSelPat_go pat Δ (ESelPure :: Hs)
......
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