Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 36 insertions, 30 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d0e26b3ba..2e74b809f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -997,7 +997,7 @@ let extern_sort s = extern_glob_sort (detype_sort s)
 
 let any_any_branch =
   (* | _ => _ *)
-  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evd.InternalHole))
+  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole))
 
 let rec glob_of_pat env = function
   | PRef ref -> GRef (loc,ref)
@@ -1010,7 +1010,7 @@ let rec glob_of_pat env = function
 	    anomaly "glob_constr_of_pattern: 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,Evd.InternalHole)
+  | PMeta None -> GHole (loc,Evar_kinds.InternalHole)
   | 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 6a9b07410..af48a37c9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -362,7 +362,7 @@ let locate_if_isevar loc na = function
       (try match na with
 	| Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> GHole (loc, Evd.BinderType na))
+      with Not_found -> GHole (loc, Evar_kinds.BinderType na))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -406,7 +406,11 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
   let env' = List.fold_left
     (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
     env fvs in
-  let bl = List.map (fun (id, loc) -> (loc, (Name id, b, None, GHole (loc, Evd.BinderType (Name id))))) fvs in
+  let bl = List.map
+    (fun (id, loc) ->
+      (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id)))))
+    fvs
+  in
   let na = match na with
     | Anonymous ->
 	if global_level then na
@@ -444,7 +448,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,Evd.BinderType na)))::bl)
+      (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na)))::bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -460,10 +464,10 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc))
+	    GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
 	else
 	  (fun (id, loc') acc ->
-	    GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc))
+	    GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -549,11 +553,11 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
             (if lassoc then List.rev l else l) termin
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
-    | AHole (Evd.BinderType (Name id as na)) ->
+    | AHole (Evar_kinds.BinderType (Name id as na)) ->
       let na =
         try snd (coerce_to_name (fst (List.assoc id terms)))
         with Not_found -> na in
-      GHole (loc,Evd.BinderType na)
+      GHole (loc,Evar_kinds.BinderType na)
     | ABinderList (x,_,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -1266,8 +1270,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,Evd.ImplicitArg (r,i,b))
-  | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
+  | 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))
   | _ -> anomaly "Only refs have implicits"
 
 let exists_implicit_name id =
@@ -1440,7 +1444,7 @@ 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 (Evd.QuestionMark (Evd.Define true))) :: l)
+	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true))) :: l)
 	  in
 	begin
 	  match cargs with
@@ -1478,9 +1482,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
 		   GCases(dummy_loc,Term.RegularStyle,Some (GSort (dummy_loc,GType None)), (* "return Type" *)
 			  List.map (fun id -> GVar (dummy_loc,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
 			  [dummy_loc,[],thepats, (* "|p1,..,pn" *)
-			   Option.cata (intern_type env') (GHole(dummy_loc,Evd.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
+			   Option.cata (intern_type env') (GHole(dummy_loc,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
 			   dummy_loc,[],list_make (List.length thepats) (PatVar(dummy_loc,Anonymous)), (* "|_,..,_" *)
-			   GHole(dummy_loc,Evd.ImpossibleCase) (* "=> _" *)]))
+			   GHole(dummy_loc,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
@@ -1503,7 +1507,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  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 -> Evd.QuestionMark (Evd.Define true))
+	GHole (loc, match k with Some k -> k | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true))
     | CPatVar (loc, n) when allow_patvar ->
 	GPatVar (loc, n)
     | CPatVar (loc, _) ->
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 7f30c6bac..c3cdd3f72 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -94,7 +94,7 @@ let anonymize_if_reserved na t = match na with
 	if not !Flags.raw_print &
 	   (try aconstr_of_glob_constr [] [] t = find_reserved_type id
             with UserError _ -> false)
-	then GHole (dummy_loc,Evd.BinderType na)
+	then GHole (dummy_loc,Evar_kinds.BinderType na)
 	else t
       with Not_found -> t)
   | Anonymous -> t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 9cad91068..1a86170f3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -31,7 +31,7 @@ type aconstr =
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
-  | AHole of Evd.hole_kind
+  | AHole of Evar_kinds.t
   | AList of identifier * identifier * aconstr * aconstr * bool
   (* Part only in glob_constr *)
   | ALambda of name * aconstr * aconstr
@@ -485,13 +485,14 @@ let rec subst_aconstr subst bound raw =
 
   | APatVar _ | ASort _ -> raw
 
-  | AHole (Evd.ImplicitArg (ref,i,b)) ->
+  | AHole (Evar_kinds.ImplicitArg (ref,i,b)) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-	  AHole (Evd.InternalHole)
-  | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
-    | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
-    | Evd.ImpossibleCase | Evd.MatchingVar _) -> raw
+	  AHole (Evar_kinds.InternalHole)
+  | AHole (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
 
   | ACast (r1,k) ->
       match k with
@@ -521,11 +522,12 @@ 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(dummy_loc,na,Explicit,GHole(dummy_loc,Evd.InternalHole),c))
+    (fun na c ->
+      GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c))
 
 let abstract_return_type_context_aconstr =
   abstract_return_type_context snd
-    (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
+    (fun na c -> ALambda(na,AHole Evar_kinds.InternalHole,c))
 
 exception No_match
 
@@ -568,7 +570,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (_,Name id2) when List.mem id2 (fst metas) ->
       let rhs = match na1 with
       | Name id1 -> GVar (dummy_loc,id1)
-      | Anonymous -> GHole (dummy_loc,Evd.InternalHole) in
+      | Anonymous -> GHole (dummy_loc,Evar_kinds.InternalHole) in
       alp, bind_env alp sigma id2 rhs
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
@@ -592,7 +594,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,Evd.BinderType na))::decls) b
+	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b
   | b -> (decls,b)
 
 let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
@@ -742,7 +744,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   | b1, ALambda (Name id,AHole _,b2) when inner ->
       let id' = Namegen.next_ident_away id (free_glob_vars b1) in
       match_in u alp metas (bind_binder sigma id
-       [(Name id',Explicit,None,GHole(dummy_loc,Evd.BinderType (Name id')))])
+       [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))])
        (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2
 
   | (GRec _ | GEvar _), _
@@ -905,7 +907,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name located option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc * Evd.hole_kind option
+  | CHole of loc * Evar_kinds.t option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * glob_sort
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a7871d41b..48871432e 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -27,7 +27,7 @@ type aconstr =
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
-  | AHole of Evd.hole_kind
+  | AHole of Evar_kinds.t
   | AList of identifier * identifier * aconstr * aconstr * bool
   (** Part only in [glob_constr] *)
   | ALambda of name * aconstr * aconstr
@@ -158,7 +158,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name located option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc * Evd.hole_kind option
+  | CHole of loc * Evar_kinds.t option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * glob_sort