Adding generic solvers to term holes. For now, no resolution mechanism nor

parsing is plugged.

35 files changed, 134 insertions, 91 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 1410cc7a0..2c4f84397 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -148,6 +148,7 @@ Impargs
 Syntax_def
 Implicit_quantifiers
 Smartlocate
+Genintern
 Constrintern
 Modintern
 Constrextern
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index 130f14717..bfc38feb8 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -70,7 +70,7 @@ EXTEND
     | "0"
       [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >>
       | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >>
-      | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False)) >>
+      | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),None) >>
       | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >>
       | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
           apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index d0fd618c7..02c00e3f0 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -161,10 +161,10 @@ let rec mlexpr_of_constr = function
     let loc = of_coqloc loc in
     <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
   | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CHole (loc, None) ->
+  | Constrexpr.CHole (loc, None, None) ->
     let loc = of_coqloc loc in
-    <:expr< Constrexpr.CHole $dloc$ None >>
-  | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
+    <:expr< Constrexpr.CHole $dloc$ None None >>
+  | Constrexpr.CHole (loc, _, _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
   | Constrexpr.CNotation(_,ntn,(subst,substl,[])) ->
       <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$
               ($mlexpr_of_list mlexpr_of_constr subst$,
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 5edfc0614..c8a0e5638 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -235,7 +235,7 @@ let constr_loc = function
   | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
-  | CHole (loc, _) -> loc
+  | CHole (loc, _, _) -> loc
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_,_) -> loc
   | CSort (loc,_) -> loc
@@ -332,14 +332,14 @@ let coerce_to_id = function
 
 let coerce_to_name = function
   | CRef (Ident (loc,id)) -> (loc,Name id)
-  | CHole (loc,_) -> (loc,Anonymous)
+  | CHole (loc,_,_) -> (loc,Anonymous)
   | a -> Errors.user_err_loc
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
 
 let rec raw_cases_pattern_expr_of_glob_constr looked_for = function
   | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_) -> RCPatAtom (loc,None)
+  | GHole (loc,_,_) -> RCPatAtom (loc,None)
   | GRef (loc,g) ->
     looked_for g;
     RCPatCstr (loc, g,[],[])
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 741ef9853..ffb8a46ea 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -597,13 +597,13 @@ let rec extern inctx scopes vars r =
 
   | GVar (loc,id) -> CRef (Ident (loc,id))
 
-  | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
+  | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None)
 
   | GEvar (loc,n,l) ->
       extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
 
   | GPatVar (loc,n) ->
-      if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
+      if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n)
 
   | GApp (loc,f,args) ->
       (match f with
@@ -748,7 +748,7 @@ let rec extern inctx scopes vars r =
 
   | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
 
-  | GHole (loc,e) -> CHole (loc, Some e)
+  | GHole (loc,e,_) -> CHole (loc, Some e, None) (** TODO: extern tactics. *)
 
   | GCast (loc,c, c') ->
       CCast (loc,sub_extern true scopes vars c,
@@ -932,7 +932,7 @@ let extern_sort s = extern_glob_sort (detype_sort s)
 
 let any_any_branch =
   (* | _ => _ *)
-  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole))
+  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None))
 
 let rec glob_of_pat env = function
   | PRef ref -> GRef (loc,ref)
@@ -945,7 +945,7 @@ let rec glob_of_pat env = function
 	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
-  | PMeta None -> GHole (loc,Evar_kinds.InternalHole)
+  | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PApp (f,args) ->
       GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b957f317a..0a2a459d3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -354,7 +354,7 @@ let locate_if_isevar loc na = function
 	| Name id -> glob_constr_of_notation_constr loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> GHole (loc, Evar_kinds.BinderType na))
+      with Not_found -> GHole (loc, Evar_kinds.BinderType na, None))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -401,7 +401,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
     env fvs in
   let bl = List.map
     (fun (id, loc) ->
-      (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id)))))
+      (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), None))))
     fvs
   in
   let na = match na with
@@ -441,7 +441,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
   | LocalRawDef((loc,na as locna),def) ->
       let indef = intern env def in
       (push_name_env lvar (impls_term_list indef) env locna,
-      (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na)))::bl)
+      (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,None)))::bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -461,10 +461,10 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
+	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), None), acc))
 	else
 	  (fun (id, loc') acc ->
-	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
+	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), None), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -562,7 +562,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
       let na =
         try snd (coerce_to_name (fst (Id.Map.find id terms)))
         with Not_found -> na in
-      GHole (loc,Evar_kinds.BinderType na)
+      GHole (loc,Evar_kinds.BinderType na,None)
     | NBinderList (x,_,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -1285,8 +1285,8 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
-  | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b))
+  | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None)
+  | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
@@ -1459,13 +1459,13 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CRecord (loc, _, fs) ->
 	let cargs =
 	  sort_fields true loc fs
-	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true))) :: l)
+	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), None) :: l)
 	  in
 	begin
 	  match cargs with
 	    | None -> user_err_loc (loc, "intern", str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (CHole (loc, None)) in
+		let pars = List.make n (CHole (loc, None, None)) in
 		let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
 	  intern env app
 	end
@@ -1497,9 +1497,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
 		   GCases(Loc.ghost,Term.RegularStyle,Some (GSort (Loc.ghost,GType None)), (* "return Type" *)
 			  List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
 			  [Loc.ghost,[],thepats, (* "|p1,..,pn" *)
-			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
+			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,None)) rtnpo; (* "=> P" is there were a P "=> _" else *)
 			   Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
-			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
+			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase,None) (* "=> _" *)]))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
@@ -1521,8 +1521,26 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
-    | CHole (loc, k) ->
-	GHole (loc, match k with Some k -> k | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true))
+    | CHole (loc, k, solve) ->
+        let k = match k with
+        | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)
+        | Some k -> k
+        in
+        let solve = match solve with
+        | None -> None
+        | Some gen ->
+          let (cvars, lvars) = fst lvar in
+          let lvars = Id.Set.union lvars cvars in
+          let ist = {
+            Genintern.ltacvars = lvars;
+            ltacrecvars = Id.Map.empty;
+            gsigma = sigma;
+            genv = globalenv;
+          } in
+          let (_, glb) = Genintern.generic_intern ist gen in
+          Some glb
+        in
+	GHole (loc, k, solve)
     | CPatVar (loc, n) when allow_patvar ->
 	GPatVar (loc, n)
     | CPatVar (loc, _) ->
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d469f36fa..10b088481 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -104,7 +104,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort (loc,x)
-  | NHole x  -> GHole (loc,x)
+  | NHole x  -> GHole (loc, x, None)
   | NPatVar n -> GPatVar (loc,(false,n))
   | NRef x -> GRef (loc,x)
 
@@ -287,7 +287,7 @@ let notation_constr_and_vars_of_glob_constr a =
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
   | GSort (_,s) -> NSort s
-  | GHole (_,w) -> NHole w
+  | GHole (_,w,_) -> NHole w
   | GRef (_,r) -> NRef r
   | GPatVar (_,(_,n)) -> NPatVar n
   | GEvar _ ->
@@ -490,7 +490,7 @@ let abstract_return_type_context pi mklam tml rtno =
 let abstract_return_type_context_glob_constr =
   abstract_return_type_context (fun (_,_,nal) -> nal)
     (fun na c ->
-      GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole),c))
+      GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,None),c))
 
 let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
@@ -553,7 +553,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (_,Name id2) when Id.List.mem id2 (fst metas) ->
       let rhs = match na1 with
       | Name id1 -> GVar (Loc.ghost,id1)
-      | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in
+      | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,None) in
       alp, bind_env alp sigma id2 rhs
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
@@ -577,7 +577,7 @@ let rec match_iterated_binders islambda decls = function
       match_iterated_binders islambda ((na,bk,None,t)::decls) b
   | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b
+	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,None))::decls) b
   | b -> (decls,b)
 
 let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
@@ -731,7 +731,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
   | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner ->
       let id' = Namegen.next_ident_away id (free_glob_vars b1) in
-      let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id')) in
+      let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),None) in
       let sigma = match t2 with
       | NHole _ -> sigma
       | NVar id2 -> bind_env alp sigma id2 t1
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 12c3dcbba..77ca9e267 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -115,7 +115,7 @@ let anonymize_if_reserved na t = match na with
             let ntn = notation_constr_of_glob_constr Id.Map.empty Id.Map.empty t in
             Pervasives.(=) ntn (find_reserved_type id) (** FIXME *)
             with UserError _ -> false)
-	then GHole (Loc.ghost,Evar_kinds.BinderType na)
+	then GHole (Loc.ghost,Evar_kinds.BinderType na,None)
 	else t
       with Not_found -> t)
   | Anonymous -> t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7c9db3ef7..cea506059 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -111,7 +111,7 @@ let fold_constr_expr_with_binders g f n acc = function
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
-      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None)) bl) acc bll
+      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None,None)) bl) acc bll
   | CGeneralization (_,_,_,c) -> f n acc c
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 68a65c5c7..64bbd1e83 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -78,7 +78,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of Loc.t * Evar_kinds.t option
+  | CHole of Loc.t * Evar_kinds.t option * Genarg.raw_generic_argument option
   | CPatVar of Loc.t * (bool * patvar)
   | CEvar of Loc.t * existential_key * constr_expr list option
   | CSort of Loc.t * glob_sort
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 315b11517..1d200ca79 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -46,7 +46,7 @@ type glob_constr =
   | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array *
       glob_constr array * glob_constr array
   | GSort of Loc.t * glob_sort
-  | GHole of (Loc.t * Evar_kinds.t)
+  | GHole of (Loc.t * Evar_kinds.t * Genarg.glob_generic_argument option)
   | GCast of Loc.t * glob_constr * glob_constr cast_type
 
 and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index a6ac42cf1..d405de921 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -47,7 +47,7 @@ open Egramml
 (** Declare Notations grammar rules                                   *)
 
 let constr_expr_of_name (loc,na) = match na with
-  | Anonymous -> CHole (loc,None)
+  | Anonymous -> CHole (loc,None,None)
   | Name id -> CRef (Ident (loc,id))
 
 let cases_pattern_expr_of_name (loc,na) = match na with
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 08c1f1917..51214d91e 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -40,17 +40,17 @@ let mk_cast = function
 let binders_of_names l =
   List.map (fun (loc, na) ->
     LocalRawAssum ([loc, na], Default Explicit,
-		   CHole (loc, Some (Evar_kinds.BinderType na)))) l
+		   CHole (loc, Some (Evar_kinds.BinderType na), None))) l
 
 let binders_of_lidents l =
   List.map (fun (loc, id) ->
     LocalRawAssum ([loc, Name id], Default Explicit,
-		  CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l
+		  CHole (loc, Some (Evar_kinds.BinderType (Name id)), None))) l
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let ty = match tyc with
       Some ty -> ty
-    | None -> CHole (loc, None) in
+    | None -> CHole (loc, None, None) in
   (id,ann,bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
@@ -60,7 +60,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
        Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
-    | None -> CHole (loc, None) in
+    | None -> CHole (loc, None, None) in
   (id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
@@ -278,7 +278,7 @@ GEXTEND Gram
       | s=sort -> CSort (!@loc,s)
       | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n))
       | s=string -> CPrim (!@loc, String s)
-      | "_" -> CHole (!@loc, None)
+      | "_" -> CHole (!@loc, None, None)
       | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
   ;
   fix_constr:
@@ -369,11 +369,11 @@ GEXTEND Gram
       | s = string -> CPatPrim (!@loc, String s) ] ]
   ;
   impl_ident_tail:
-    [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None))
+    [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None, None))
     | idl=LIST1 name; ":"; c=lconstr; "}" ->
         (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
     | idl=LIST1 name; "}" ->
-        (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None)))
+        (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None, None)))
     | ":"; c=lconstr; "}" ->
 	(fun id -> LocalRawAssum ([id],Default Implicit,c))
     ] ]
@@ -404,7 +404,7 @@ GEXTEND Gram
           binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
           [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2],
-	                  Default Explicit,CHole (!@loc,None))]
+	                  Default Explicit,CHole (!@loc, None, None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
     ] ]
@@ -413,7 +413,7 @@ GEXTEND Gram
     [ [ l = LIST0 binder -> List.flatten l ] ]
   ;
   binder:
-    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None))]
+    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, None))]
       | bl = closed_binder -> bl ] ]
   ;
   closed_binder:
@@ -426,13 +426,13 @@ GEXTEND Gram
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
           [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))]
       | "{"; id=name; "}" ->
-          [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))]
+          [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
           [LocalRawAssum (id::idl,Default Implicit,c)]
       | "{"; id=name; ":"; c=lconstr; "}" ->
           [LocalRawAssum ([id],Default Implicit,c)]
       | "{"; id=name; idl=LIST1 name; "}" ->
-          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))) (id::idl)
+          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, None))) (id::idl)
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
 	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index d075a7790..c2dbd1d63 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -192,7 +192,7 @@ GEXTEND Gram
 	      | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None))) ty)
+	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, None))) ty)
     ] ]
   ;
   match_context_rule:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b72bb0264..eb483c50c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -424,7 +424,7 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None))
+    [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None, None))
       | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 81bd6a108..567bde9ca 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -323,7 +323,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c
-      | -> CHole (!@loc, None) ] ]
+      | -> CHole (!@loc, None, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -372,7 +372,7 @@ GEXTEND Gram
 	     (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None)))
+    [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -391,7 +391,7 @@ GEXTEND Gram
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None)))) ]
+		 fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None, None)))) ]
 	 -> t l
      ]]
 ;
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index bbac10f0f..a722daca5 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -187,7 +187,7 @@ let interp_constr_or_thesis check_sort sigma env = function
 let abstract_one_hyp inject h glob =
   match h with
       Hvar (loc,(id,None)) ->
-	GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob)
+	GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), None), glob)
     | Hvar (loc,(id,Some typ)) ->
 	GProd (Loc.ghost,Name id, Explicit, fst typ, glob)
     | Hprop st ->
@@ -245,7 +245,7 @@ let rec glob_of_pat =
 	let rec add_params n q =
 	  if n<=0 then q else
 	    add_params (pred n) (GHole(Loc.ghost,
-				       Evar_kinds.TomatchTypeParameter(ind,n))::q) in
+				       Evar_kinds.TomatchTypeParameter(ind,n), None)::q) in
 	    let args = List.map glob_of_pat lpat in
 	      glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr),
 		   add_params mind.Declarations.mind_nparams args)
@@ -254,14 +254,14 @@ let prod_one_hyp = function
     (loc,(id,None)) ->
       (fun glob ->
 	 GProd (Loc.ghost,Name id, Explicit,
-		GHole (loc,Evar_kinds.BinderType (Name id)), glob))
+		GHole (loc,Evar_kinds.BinderType (Name id), None), glob))
   | (loc,(id,Some typ)) ->
       (fun glob ->
 	 GProd (Loc.ghost,Name id, Explicit, fst typ, glob))
 
 let prod_one_id (loc,id) glob =
   GProd (Loc.ghost,Name id, Explicit,
-	 GHole (loc,Evar_kinds.BinderType (Name id)), glob)
+	 GHole (loc,Evar_kinds.BinderType (Name id), None), glob)
 
 let let_in_one_alias (id,pat) glob =
   GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob)
@@ -342,7 +342,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	   GVar (loc,id)) params in
     let dum_args=
       List.init oib.Declarations.mind_nrealargs
-	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) in
+	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),None)) in
       glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
@@ -417,7 +417,7 @@ let abstract_one_arg = function
     (loc,(id,None)) ->
       (fun glob ->
 	 GLambda (Loc.ghost,Name id, Explicit,
-		GHole (loc,Evar_kinds.BinderType (Name id)), glob))
+		GHole (loc,Evar_kinds.BinderType (Name id),None), glob))
   | (loc,(id,Some typ)) ->
       (fun glob ->
 	 GLambda (Loc.ghost,Name id, Explicit, fst typ, glob))
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index db53dc932..b21037d25 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)
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)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 79cba2c7c..6a7f326e6 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -18,7 +18,7 @@ let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b)
 let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b)
 let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl)
 let mkGSort s = GSort(Loc.ghost,s)
-let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous)
+let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,None)
 let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t)
 
 (*
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 1cce6cd70..b8c2b33fd 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -165,10 +165,10 @@ let word_of_pos_bigint dloc hght n =
     if hgt <= 0 then
       int31_of_pos_bigint dloc n
     else if equal n zero then
-      GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole)])
+      GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, None)])
     else
       let (h,l) = split_at hgt n in
-      GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole);
+      GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, None);
 			   decomp (hgt-1) h;
 			   decomp (hgt-1) l])
   in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c9280582b..a5e822862 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1920,7 +1920,7 @@ let mk_JMeq typ x typ' y =
   mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |])
 
-let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true))
+let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4e0fc5de6..c29c443b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -591,6 +591,8 @@ let rec subst_cases_pattern subst pat =
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
 
+let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
+
 let rec subst_glob_constr subst raw =
   match raw with
   | GRef (loc,ref) ->
@@ -674,14 +676,16 @@ let rec subst_glob_constr subst raw =
 
   | GSort _ -> raw
 
-  | GHole (loc,Evar_kinds.ImplicitArg (ref,i,b)) ->
-      let ref',_ = subst_global subst ref in
-	if ref' == ref then raw else
-	  GHole (loc,Evar_kinds.InternalHole)
-  | GHole (loc, (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _
-		|Evar_kinds.CasesType |Evar_kinds.InternalHole
-		|Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar
-		|Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _)) -> raw
+  | GHole (loc, knd, solve) ->
+    let nknd = match knd with
+    | Evar_kinds.ImplicitArg (ref, i, b) ->
+      let nref, _ = subst_global subst ref in
+      if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
+    | _ -> knd
+    in
+    let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in
+    if nsolve == solve && nknd = knd then raw
+    else GHole (loc, nknd, nsolve)
 
   | GCast (loc,r1,k) ->
       let r1' = subst_glob_constr subst r1 in
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cb478777f..97c636af7 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -60,6 +60,9 @@ val simple_cases_matrix_of_branches :
 val return_type_of_predicate :
   inductive -> int -> glob_constr -> predicate_pattern * glob_constr option
 
+val subst_genarg_hook :
+  (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
+
 module PrintingInductiveMake :
   functor (Test : sig
     val encode : Libnames.reference -> Names.inductive
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 94ff780ec..b847a1390 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -245,7 +245,7 @@ let loc_of_glob_constr = function
   | GIf (loc,_,_,_,_) -> loc
   | GRec (loc,_,_,_,_,_) -> loc
   | GSort (loc,_) -> loc
-  | GHole (loc,_) -> loc
+  | GHole (loc,_,_) -> loc
   | GCast (loc,_,_) -> loc
 
 (**********************************************************************)
@@ -259,7 +259,7 @@ let rec cases_pattern_of_glob_constr na = function
       raise Not_found
     | Anonymous -> PatVar (loc,Name id)
     end
-  | GHole (loc,_) -> PatVar (loc,na)
+  | GHole (loc,_,_) -> PatVar (loc,na)
   | GRef (loc,ConstructRef cstr) ->
       PatCstr (loc,cstr,[],na)
   | GApp (loc,GRef (_,ConstructRef cstr),l) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 79e3913a9..a2e8e4599 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -340,7 +340,7 @@ let rec pat_of_raw metas vars = function
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (loc,nal,(_,None),b,c) ->
       let mkGLambda c na =
-	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole),c) in
+	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, None),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 05968b6be..a7e1cf481 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -288,6 +288,8 @@ let pretype_sort evdref = function
 let new_type_evar evdref env loc =
   evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref
 
+let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
+
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
@@ -321,13 +323,24 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
       let k = Evar_kinds.MatchingVar (someta,n) in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-  | GHole (loc,k) ->
+  | GHole (loc, k, None) ->
       let ty =
         match tycon with
         | Some ty -> ty
         | None ->
-	    new_type_evar evdref env loc in
-	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+          new_type_evar evdref env loc in
+        { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+
+  | GHole (loc, k, Some arg) ->
+      let ty =
+        match tycon with
+        | Some ty -> ty
+        | None ->
+          new_type_evar evdref env loc in
+      let ist = snd lvar in
+      let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
+      let () = evdref := sigma in
+      { uj_val = c; uj_type = ty }
 
   | GRec (loc,fixkind,names,bl,lar,vdef) ->
       let rec type_bl env ctxt = function
@@ -717,7 +730,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
 and pretype_type valcon env evdref lvar = function
-  | GHole loc ->
+  | GHole (loc, knd, None) ->
       (match valcon with
        | Some v ->
            let s =
@@ -733,7 +746,7 @@ and pretype_type valcon env evdref lvar = function
 	       utj_type = s }
        | None ->
 	   let s = evd_comb0 new_sort_variable evdref in
-	     { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
+	     { utj_val = e_new_evar evdref env ~src:(loc, knd) (mkSort s);
 	       utj_type = s})
   | c ->
       let j = pretype empty_tycon env evdref lvar c in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 98306e57f..dd02423a8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -125,3 +125,7 @@ val constr_out : Dyn.t -> constr
 
 val interp_sort : glob_sort -> sorts
 val interp_elimination_sort : glob_sort -> sorts_family
+
+val genarg_interp_hook :
+  (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t ->
+    Genarg.glob_generic_argument -> constr * evar_map) Hook.t
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index b389ca790..92b4bf496 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -258,7 +258,7 @@ let pr_binder_among_many pr_c = function
   | LocalRawDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t
-        | _ -> c, CHole (Loc.ghost, None) in
+        | _ -> c, CHole (Loc.ghost, None, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 441e362b1..ba640863d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -250,7 +250,7 @@ let pr_module_binders l pr_c =
   prlist_strict (pr_module_vardecls pr_c) l
 
 let pr_type_option pr_c = function
-  | CHole (loc, k) -> mt()
+  | CHole (loc, k, _) -> mt()
   | _ as c -> brk(0,2) ++ str":" ++ pr_c c
 
 let pr_decl_notation prc ((loc,ntn),c,scopt) =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1c7b8d49f..c81e7ce3f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -554,7 +554,7 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
 	      GHole (Loc.make_loc (!locref,0),
-		     Evar_kinds.QuestionMark(Evar_kinds.Define true))))
+		     Evar_kinds.QuestionMark(Evar_kinds.Define true), None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
   let t' = substrec t
@@ -565,13 +565,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) ->
+    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
 	   GHole (Loc.make_loc (!locref,0),
-		  Evar_kinds.QuestionMark(Evar_kinds.Define true)))
+		  Evar_kinds.QuestionMark(Evar_kinds.Define true),s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 337ae5241..2e3b6e1af 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1511,7 +1511,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CHole (Loc.ghost, None)
+let cHole = CHole (Loc.ghost, None, None)
 
 let proper_projection r ty =
   let ctx, inst = decompose_prod_assum ty in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 728baadb4..bb34323cd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -127,7 +127,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	  (fun avoid (clname, (id, _, t)) ->
 	    match clname with
 	    | Some (cl, b) ->
-		let t = CHole (Loc.ghost, None) in
+		let t = CHole (Loc.ghost, None, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -228,7 +228,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Loc.ghost, Some Evar_kinds.GoalEvar) :: props), rest
+		       (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, None) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 095bf5300..77219f9a2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -50,7 +50,7 @@ let rec under_binders env f n c =
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
   | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
-  | CHole (loc, k) ->
+  | CHole (loc, k, _) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
 	user_err_loc (loc,"",
diff --git a/toplevel/record.ml b/toplevel/record.ml
index cf5714546..2ef425bf2 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -43,7 +43,7 @@ let interp_fields_evars evars env impls_env nots l =
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
-  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))
+  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, None))
 
 let binders_of_decls = List.map binder_of_decl