Commit a68ee609 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Turn some matches into lazymatches to improve error propagation.

parent 4cba2266
...@@ -676,7 +676,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := ...@@ -676,7 +676,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let rec find_pat found pats := let rec find_pat found pats :=
lazymatch pats with lazymatch pats with
| [] => | [] =>
match found with lazymatch found with
| true => idtac | true => idtac
| false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern" | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end end
...@@ -684,7 +684,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := ...@@ -684,7 +684,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IClear ?H :: ?pats => iClear H; find_pat found pats | IClear ?H :: ?pats => iClear H; find_pat found pats
| IClearFrame ?H :: ?pats => iFrame H; find_pat found pats | IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
| ?pat :: ?pats => | ?pat :: ?pats =>
match found with lazymatch found with
| false => go H pat; find_pat true pats | false => go H pat; find_pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern" | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end end
......
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