Skip to content
Snippets Groups Projects
Commit 6da588fd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Let `sel_pat.parse` fail with proper error when type is incorrect.

parent 3cb65333
No related branches found
No related tags found
No related merge requests found
...@@ -39,5 +39,6 @@ Ltac parse s := ...@@ -39,5 +39,6 @@ Ltac parse s :=
lazymatch eval vm_compute in (parse s) with lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid sel_pat" s | Some ?pats => pats | _ => fail "invalid sel_pat" s
end end
| ?X => fail "sel_pat.parse:" s "has unexpected type" X
end. end.
End sel_pat. End sel_pat.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment