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

19 files changed, 66 insertions, 97 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index cc4b3f07f6..7019495afb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -278,8 +278,8 @@ let rec find_row_ind = function
 let inductive_template evdref env tmloc ind =
   let arsign = get_full_arity_sign env ind in
   let hole_source = match tmloc with
-    | Some loc -> fun i -> (loc, TomatchTypeParameter (ind,i))
-    | None -> fun _ -> (dummy_loc, InternalHole) in
+    | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
+    | None -> fun _ -> (dummy_loc, Evar_kinds.InternalHole) in
    let (_,evarl,_) =
     List.fold_right
       (fun (na,b,ty) (subst,evarl,n) ->
@@ -357,7 +357,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
 (************************************************************************)
 (* Utils *)
 
-let mkExistential env ?(src=(dummy_loc,InternalHole)) evdref =
+let mkExistential env ?(src=(dummy_loc,Evar_kinds.InternalHole)) evdref =
   e_new_evar evdref env ~src:src (new_Type ())
 
 let evd_comb2 f evdref x y =
@@ -909,7 +909,7 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
 let adjust_impossible_cases pb pred tomatch submat =
   if submat = [] then
     match kind_of_term (whd_evar !(pb.evdref) pred) with
-    | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase ->
+    | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = Evar_kinds.ImpossibleCase ->
 	let default = (coq_unit_judge ()).uj_type in
 	pb.evdref := Evd.define evk default !(pb.evdref);
       (* we add an "assert false" case *)
@@ -1469,7 +1469,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ev = e_new_evar evdref env ~src:(loc, CasesType) ty in
+        let ev = e_new_evar evdref env ~src:(loc, Evar_kinds.CasesType) ty in
         evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref;
         ev
     | _ ->
@@ -1492,7 +1492,8 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       let filter = rel_filter@named_filter in
       let candidates = u :: List.map mkRel vl in
       let ev =
-	e_new_evar evdref extenv ~src:(loc, CasesType) ~filter ~candidates ty in
+	e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType)
+	  ~filter ~candidates ty in
       lift k ev
     else
       map_constr_with_full_binders push_binder aux x t in
@@ -1507,7 +1508,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
 	let n' = rel_context_length (rel_context tycon_env) in
         let tt = new_Type () in
 	let impossible_case_type =
-	  e_new_evar evdref env ~src:(loc,ImpossibleCase) tt in
+	  e_new_evar evdref env ~src:(loc,Evar_kinds.ImpossibleCase) tt in
 	(lift (n'-n) impossible_case_type, tt)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
@@ -1759,7 +1760,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
 	(* we use two strategies *)
         let sigma,t = match tycon with
 	| Some t -> sigma,t
-	| None -> new_type_evar sigma env ~src:(loc, CasesType) in
+	| None -> new_type_evar sigma env ~src:(loc, Evar_kinds.CasesType) in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Second strategy: we directly use the evar as a non dependent pred *)
@@ -1825,7 +1826,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 (dummy_loc, Evd.QuestionMark (Evd.Define true))
+let hole = GHole (dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define true))
 
 let constr_of_pat env isevars arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 60e10ac8ef..34eb92fa04 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -66,8 +66,8 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
 
 open Program
 
-let make_existential loc ?(opaque = Define true) env isevars c =
-  Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c
+let make_existential loc ?(opaque = Evar_kinds.Define true) env isevars c =
+  Evarutil.e_new_evar isevars env ~src:(loc, Evar_kinds.QuestionMark opaque) c
 
 let app_opt env evars f t =
   whd_betaiota !evars (app_opt f t)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 99d054e565..33e1ecdf22 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -658,13 +658,14 @@ let rec subst_glob_constr subst raw =
 
   | GSort _ -> raw
 
-  | GHole (loc,ImplicitArg (ref,i,b)) ->
+  | GHole (loc,Evar_kinds.ImplicitArg (ref,i,b)) ->
       let ref',_ = subst_global subst ref in
 	if ref' == ref then raw else
-	  GHole (loc,InternalHole)
-  | GHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
-      TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) ->
-      raw
+	  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
 
   | GCast (loc,r1,k) ->
       (match k with
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cddfbd5d14..ab11df450e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -540,7 +540,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
     List.fold_left
       (fun (i,ks,m) b ->
 	 if m=n then (i,t2::ks, m-1) else
-	 let dloc = (dummy_loc,InternalHole) in
+	 let dloc = (dummy_loc,Evar_kinds.InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
 	 (i', ev :: ks, m - 1))
       (evd,[],List.length bs - 1) bs
@@ -816,7 +816,7 @@ let rec solve_unconstrained_evars_with_canditates evd =
 let solve_unconstrained_impossible_cases evd =
   Evd.fold_undefined (fun evk ev_info evd' ->
     match ev_info.evar_source with
-    | _,ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd'
+    | _,Evar_kinds.ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd'
     | _ -> evd') evd evd
 
 let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index da99436cad..84a1cd550f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -308,7 +308,7 @@ let push_rel_context_to_named_context env typ =
  * Entry points to define new evars   *
  *------------------------------------*)
 
-let default_source = (dummy_loc,InternalHole)
+let default_source = (dummy_loc,Evar_kinds.InternalHole)
 
 let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
   let newevk = new_untyped_evar() in
@@ -338,7 +338,7 @@ let new_type_evar ?src ?filter evd env =
   new_evar evd' env ?src ?filter (mkSort s)
 
   (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
+let e_new_evar evdref env ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates ty =
   let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
   evdref := evd';
   ev
@@ -1874,7 +1874,7 @@ let check_evars env initial_sigma sigma c =
 	  if not (Evd.mem initial_sigma evk) then
             let (loc,k) = evar_source evk sigma in
 	      match k with
-	      | ImplicitArg (gr, (i, id), false) -> ()
+	      | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
 	      | _ ->
 		  let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
 		    error_unsolvable_implicit loc env sigma evi k None)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index bef5398aab..82d154d399 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -30,18 +30,18 @@ val new_untyped_evar : unit -> existential_key
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list ->
+  evar_map -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list ->
   ?candidates:constr list -> types -> evar_map * constr
 
 (** the same with side-effects *)
 val e_new_evar :
-  evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list ->
+  evar_map ref -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list ->
   ?candidates:constr list -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  ?src:loc * hole_kind -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+  ?src:loc * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -50,7 +50,7 @@ val new_type_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index f1c278bd2d..5164385ce3 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -18,24 +18,11 @@ open Environ
 open Libnames
 open Mod_subst
 
-(* The kinds of existential variable *)
-
-type obligation_definition_status = Define of bool | Expand
-
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option) * bool
-  | BinderType of name
-  | QuestionMark of obligation_definition_status
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-  | GoalEvar
-  | ImpossibleCase
-  | MatchingVar of bool * identifier
+(* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
 
-type evar = existential_key
+type evar = Term.existential_key
 
 let string_of_existential evk = "?" ^ string_of_int evk
 let existential_of_int evk = evk
@@ -49,7 +36,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   evar_filter : bool list;
-  evar_source : hole_kind located;
+  evar_source : Evar_kinds.t located;
   evar_candidates : constr list option; (* if not None, list of allowed instances *)
   evar_extra : Store.t }
 
@@ -58,7 +45,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
-  evar_source = (dummy_loc,InternalHole);
+  evar_source = (dummy_loc,Evar_kinds.InternalHole);
   evar_candidates = None;
   evar_extra = Store.empty
 }
@@ -432,7 +419,7 @@ let define evk body evd =
 	| [] ->  evd.last_mods
         | _ -> ExistentialSet.add evk evd.last_mods }
 
-let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter ?candidates evd =
+let evar_declare hyps evk ty ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates evd =
   let filter =
     if filter = None then
       List.map (fun _ -> true) (named_context_of_val hyps)
@@ -752,20 +739,20 @@ let pr_decl ((id,b,_),ok) =
       print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
-  | QuestionMark _ -> str "underscore"
-  | CasesType -> str "pattern-matching return predicate"
-  | BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
-  | BinderType Anonymous -> str "type of anonymous binder"
-  | ImplicitArg (c,(n,ido),b) ->
+  | Evar_kinds.QuestionMark _ -> str "underscore"
+  | Evar_kinds.CasesType -> str "pattern-matching return predicate"
+  | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
+  | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+  | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
       str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
       spc () ++ print_constr (constr_of_global c)
-  | InternalHole -> str "internal placeholder"
-  | TomatchTypeParameter (ind,n) ->
+  | Evar_kinds.InternalHole -> str "internal placeholder"
+  | Evar_kinds.TomatchTypeParameter (ind,n) ->
       pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
-  | GoalEvar -> str "goal evar"
-  | ImpossibleCase -> str "type of impossible pattern-matching clause"
-  | MatchingVar _ -> str "matching variable"
+  | Evar_kinds.GoalEvar -> str "goal evar"
+  | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
+  | Evar_kinds.MatchingVar _ -> str "matching variable"
 
 let pr_evar_info evi =
   let phyps =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index bfdbf5e716..ca552a450b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -73,26 +73,6 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 
 
 (********************************************************************
-  ** Kinds of existential variables ***)
-
-(** Should the obligation be defined (opaque or transparent (default)) or
-   defined transparent and expanded in the term? *)
-
-type obligation_definition_status = Define of bool | Expand
-
-(** Evars *)
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option) * bool (** Force inference *)
-  | BinderType of name
-  | QuestionMark of obligation_definition_status
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-  | GoalEvar
-  | ImpossibleCase
-  | MatchingVar of bool * identifier
-
-(********************************************************************
   ** Existential variables and unification states ***)
 
 (** A unification state (of type [evar_map]) is primarily a finite mapping
@@ -118,7 +98,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   evar_filter : bool list;
-  evar_source : hole_kind located;
+  evar_source : Evar_kinds.t located;
   evar_candidates : constr list option;
   evar_extra : Store.t }
 
@@ -199,9 +179,9 @@ val defined_evars : evar_map -> evar_map
     It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val evar_declare :
-  named_context_val -> evar -> types -> ?src:loc * hole_kind ->
+  named_context_val -> evar -> types -> ?src:loc * Evar_kinds.t ->
       ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
-val evar_source : existential_key -> evar_map -> hole_kind located
+val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 
 (* spiwack: this function seems to somewhat break the abstraction. 
    [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 616a854444..fc1e1247f9 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -15,7 +15,6 @@ open Sign
 open Term
 open Libnames
 open Nametab
-open Evd
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -67,7 +66,7 @@ type glob_constr =
   | GRec of loc * fix_kind * identifier array * glob_decl list array *
       glob_constr array * glob_constr array
   | GSort of loc * glob_sort
-  | GHole of (loc * hole_kind)
+  | GHole of (loc * Evar_kinds.t)
   | GCast of loc * glob_constr * glob_constr cast_type
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index fca66fd28d..d7d182833b 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -70,7 +70,7 @@ type glob_constr =
   | GRec of loc * fix_kind * identifier array * glob_decl list array *
       glob_constr array * glob_constr array
   | GSort of loc * glob_sort
-  | GHole of (loc * Evd.hole_kind)
+  | GHole of (loc * Evar_kinds.t)
   | GCast of loc * glob_constr * glob_constr cast_type
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 0610c00f14..47cc57fd1d 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -111,7 +111,7 @@ let pattern_of_constr sigma t =
           match kind_of_term f with
             Evar (evk,args as ev) ->
               (match snd (Evd.evar_source evk sigma) with
-                  MatchingVar (true,id) ->
+                  Evar_kinds.MatchingVar (true,id) ->
                     ctx := (id,None,existential_type sigma ev)::!ctx;
                     Some id
                 | _ -> None)
@@ -124,10 +124,10 @@ let pattern_of_constr sigma t =
     | Construct sp -> PRef (canonical_gr (ConstructRef sp))
     | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
-          | MatchingVar (b,id) ->
+          | Evar_kinds.MatchingVar (b,id) ->
               ctx := (id,None,existential_type sigma ev)::!ctx;
               assert (not b); PMeta (Some id)
-          | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
+          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
@@ -308,7 +308,8 @@ let rec pat_of_raw metas vars = function
       PIf (pat_of_raw metas vars c,
            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,Evd.InternalHole),c) in
+      let mkGLambda c na =
+	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 409e405f5c..e0cc2dec37 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -24,8 +24,8 @@ type pretype_error =
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * Evd.hole_kind
-  | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
+  | NotClean of existential_key * constr * Evar_kinds.t
+  | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
       Evd.unsolvability_explanation option
   | CannotUnify of constr * constr
   | CannotUnifyLocal of constr * constr * constr
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 43f934520d..7debe2b0d1 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -23,8 +23,8 @@ type pretype_error =
   | CantFindCaseType of constr
   (** Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * Evd.hole_kind
-  | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
+  | NotClean of existential_key * constr * Evar_kinds.t
+  | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
       Evd.unsolvability_explanation option
   | CannotUnify of constr * constr
   | CannotUnifyLocal of constr * constr * constr
@@ -95,10 +95,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
-  env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
+  env -> Evd.evar_map -> existential_key -> constr -> loc * Evar_kinds.t -> 'b
 
 val error_unsolvable_implicit :
-  loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind ->
+  loc -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
       Evd.unsolvability_explanation option -> 'b
 
 val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0205a52d5d..d2553828f4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -245,7 +245,7 @@ let pretype_sort evdref = function
 exception Found of fixpoint
 
 let new_type_evar evdref env loc =
-  evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref
+  evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref
 
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
@@ -277,7 +277,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
         match tycon with
         | Some ty -> ty
         | None -> new_type_evar evdref env loc in
-      let k = MatchingVar (someta,n) in
+      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) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e6005391da..6be28ebcbe 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -451,7 +451,7 @@ let is_instance = function
       is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg k = k <> GoalEvar
+let is_implicit_arg k = k <> Evar_kinds.GoalEvar
   (* match k with *)
   (*     ImplicitArg (ref, (n, id), b) -> true *)
   (*   | InternalHole -> true *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b1db243d67..7e283e56d5 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -72,7 +72,7 @@ val instance_impl : instance -> global_reference
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
 
-val is_implicit_arg : hole_kind -> bool
+val is_implicit_arg : Evar_kinds.t -> bool
 
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index f6de344a97..6429116de7 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -28,7 +28,7 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
+    | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fd709763d1..3feb652ae3 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -25,7 +25,7 @@ type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * identifier located (** Class name, method *)
   | NoInstance of identifier located * constr list
-  | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
+  | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ce0af6853a..2344f6e46e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -113,7 +113,7 @@ let pose_all_metas_as_evars env evd t =
        | None ->
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if mvs = Evd.Metaset.empty then ty else aux ty in
-        let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in
+        let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in
         evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
         ev)
   | _ ->
@@ -774,7 +774,7 @@ let applyHead env evd n c  =
       match kind_of_term (whd_betadeltaiota env evd cty) with
       | Prod (_,c1,c2) ->
         let (evd',evar) =
-	  Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
+	  Evarutil.new_evar evd env ~src:(dummy_loc,Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
       | _ -> error "Apply_Head_Then"
   in