From 6da588fd41047fd6455dc114bef617aeb21e6e88 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 14 Jun 2021 12:26:55 +0200
Subject: [PATCH] Let `sel_pat.parse` fail with proper error when type is
incorrect.
---
iris/proofmode/sel_patterns.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/iris/proofmode/sel_patterns.v b/iris/proofmode/sel_patterns.v
index 6f498a365..4f74efe1b 100644
--- a/iris/proofmode/sel_patterns.v
+++ b/iris/proofmode/sel_patterns.v
@@ -39,5 +39,6 @@ Ltac parse s :=
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid sel_pat" s
end
+ | ?X => fail "sel_pat.parse:" s "has unexpected type" X
end.
End sel_pat.
--
GitLab