From 144f2ac7c7394a701808daa503a0b6ded5663fcc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/firstorder/instances.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder/instances.ml')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index d34edb863..e856326c8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -125,7 +125,7 @@ let mk_open_instance id gl m t=
       match t with
 	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1)
+	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1)
 	| _-> anomaly (Pp.str "can't happen") in
   let ntt=try
     Pretyping.understand evmap env (raux m rawt)
-- 
cgit v1.2.3