From 85509592a26faddb24e077267802c7b570586d3d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jan 2019 08:09:39 +0000
Subject: [PATCH] Correctly coerce `ident` into `spec_pat` in `spec_pat.parse`.
This became broken after the nested iSpecialize MR.
---
theories/proofmode/spec_patterns.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 771f09e81..2c0ca4725 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -95,7 +95,7 @@ Ltac parse s :=
| string => lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "spec_pat.parse: cannot parse" s
end
- | ident => constr:([SIdent s])
+ | ident => constr:([SIdent s []])
| ?X => fail "spec_pat.parse:" s "has unexpected type" X
end.
End spec_pat.
--
GitLab