hiding the meta_map in evar_defs

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

5 files changed, 16 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 372b6c4ed..77853ade8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1231,10 +1231,10 @@ let rec cases_pattern_expr_of_constr_expr = function
 
 let rec rawconstr_of_cases_pattern = function
   | PatVar (loc,Name id) -> RVar (loc,id)
-  | PatVar (loc,Anonymous) -> RHole (loc,InternalHole)
+  | PatVar (loc,Anonymous) -> RHole (loc,Evd.InternalHole)
   | PatCstr (loc,(ind,_ as c),args,_) -> 
       let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
-      let params = list_tabulate (fun _ -> RHole (loc,InternalHole)) nparams in
+      let params = list_tabulate (fun _ -> RHole (loc,Evd.InternalHole)) nparams in
       let args = params @ List.map rawconstr_of_cases_pattern args in
       let f = RRef (loc,ConstructRef c) in
       if args = [] then f else RApp (loc,f,args)
@@ -1573,7 +1573,7 @@ let rec extern inctx scopes vars r =
 	(sub_extern false scopes vars tm,
 	(na',option_app (fun (loc,ind,nal) ->
 	  let args = List.map (function
-	    | Anonymous -> RHole (dummy_loc,InternalHole) 
+	    | Anonymous -> RHole (dummy_loc,Evd.InternalHole) 
 	    | Name id -> RVar (dummy_loc,id)) nal in
 	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
 	  (extern_type scopes vars t)) x))) tml in
@@ -1794,7 +1794,7 @@ let rec raw_of_pat tenv env = function
 	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
       with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in
       RVar (loc,id)
-  | PMeta None -> RHole (loc,InternalHole)
+  | PMeta None -> RHole (loc,Evd.InternalHole)
   | PMeta (Some n) -> RPatVar (loc,(false,n))
   | PApp (f,args) ->
       RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 03cd671af..28f0de932 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -625,7 +625,7 @@ let locate_if_isevar loc na = function
       (try match na with
 	| Name id ->  Reserve.find_reserved_type id
 	| Anonymous -> raise Not_found 
-      with Not_found -> RHole (loc, BinderType na))
+      with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
 
 let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
@@ -669,8 +669,8 @@ let get_implicit_name n imps =
   else Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i = function
-  | RRef (loc,r) -> (loc,ImplicitArg (r,i))
-  | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
+  | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
+  | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
   | _ -> anomaly "Only refs have implicits"
 
 let exists_implicit_name id =
@@ -908,7 +908,7 @@ let internalise sigma env allow_soapp lvar c =
         let p' = option_app (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
-	RHole (loc, QuestionMark)
+	RHole (loc, Evd.QuestionMark)
     | CPatVar (loc, n) when allow_soapp ->
 	RPatVar (loc, n)
     | CPatVar (loc, (false,n)) when Options.do_translate () ->
@@ -943,7 +943,7 @@ let internalise sigma env allow_soapp lvar c =
           (env,bl) nal
     | LocalRawDef((loc,na),def) ->
         ((name_fold Idset.add na ids,ts,sc),
-         (na,Some(intern env def),RHole(loc,BinderType na))::bl)
+         (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
   and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
     let idsl_pll = List.map (intern_cases_pattern scopes ([],[]) None) lhs in
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 167f492c8..14797930d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -89,7 +89,7 @@ let anonymize_if_reserved na t = match na with
       if !Options.v7 & id = id_of_string "_" then t else
       (try 
 	if unloc t = find_reserved_type id
-	then RHole (dummy_loc,BinderType na)
+	then RHole (dummy_loc,Evd.BinderType na)
 	else t
       with Not_found -> t)
   | Anonymous -> t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3b72ef78..8f9360e57 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -43,7 +43,7 @@ type aconstr =
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
-  | AHole of hole_kind
+  | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * aconstr
   
@@ -192,12 +192,12 @@ let rec subst_aconstr subst raw =
 
   | APatVar _ | ASort _ -> raw
 
-  | AHole (ImplicitArg (ref,i)) ->
+  | AHole (Evd.ImplicitArg (ref,i)) ->
       let ref' = subst_global subst ref in 
 	if ref' == ref then raw else
-	  AHole (ImplicitArg (ref',i))
-  | AHole (BinderType _ | QuestionMark | CasesType |
-      InternalHole | TomatchTypeParameter _) -> raw
+	  AHole (Evd.ImplicitArg (ref',i))
+  | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType |
+      Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
 
   | ACast (r1,r2) -> 
       let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d5046b43b..53182e34b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -39,7 +39,7 @@ type aconstr =
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
-  | AHole of hole_kind
+  | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * aconstr