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

parsing is plugged.

5 files changed, 17 insertions, 17 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index a6ac42cf16..d405de921f 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 08c1f19170..51214d91ea 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 d075a77904..c2dbd1d63e 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 b72bb02641..eb483c50cf 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 81bd6a1084..567bde9cac 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
      ]]
 ;