From 144f2ac7c7394a701808daa503a0b6ded5663fcc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Sep 2013 21:50:35 +0200
Subject: Adding generic solvers to term holes. For now, no resolution
 mechanism nor parsing is plugged.

---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode/decl_proof_instr.ml')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index db53dc9320..b21037d252 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1276,7 +1276,7 @@ let understand_my_constr c gls =
   let nc = names_of_rel_context env in
   let rawc = Detyping.detype false [] nc c in
   let rec frob = function
-    | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand)
+    | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None)
     | rc ->  map_glob_constr frob rc
   in
   Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
-- 
cgit v1.2.3