From 8f5e1e166e7e174ff393a2a8fa2b11188745b19e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2020 17:06:44 +0200
Subject: Ssrmatching: Hack to circumvent a hack.

---
 plugins/ssrmatching/ssrmatching.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index adaf7c8cc1..ce6fd4939b 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -370,6 +370,11 @@ let ehole_var = EConstr.mkVar (Id.of_string "_")
 let pr_econstr_pat env sigma c0 =
   let rec wipe_evar c = let open EConstr in
     if isEvar sigma c then ehole_var else map sigma wipe_evar c in
+  let dummy_decl =
+    let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in
+    let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in
+    Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in
+  let env = Environ.push_named dummy_decl env in
   pr_econstr_env env sigma (wipe_evar c0)
 
 (* Turn (new) evars into metas *)
-- 
cgit v1.2.3