Standardisation du nom des méthodes de Evd

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

6 files changed, 32 insertions, 34 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2785d08389..658bf407f7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -35,7 +35,7 @@ exception Uninstantiated_evar of existential_key
 
 let rec whd_ise sigma c =
   match kind_of_term c with
-    | Evar (ev,args) when Evd.in_dom sigma ev ->
+    | Evar (ev,args) when Evd.mem sigma ev ->
 	if Evd.is_defined sigma ev then
           whd_ise sigma (existential_value sigma (ev,args))
 	else raise (Uninstantiated_evar ev)
@@ -46,7 +46,7 @@ let rec whd_ise sigma c =
 let whd_castappevar_stack sigma c = 
   let rec whrec (c, l as s) =
     match kind_of_term c with
-      | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
+      | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> 
 	  whrec (existential_value sigma (ev,args), l)
       | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
@@ -93,7 +93,7 @@ let collect_evars emap c =
   let rec collrec acc c =
     match kind_of_term c with
       | Evar (k,_) ->
-	  if Evd.in_dom emap k & not (Evd.is_defined emap k) then k::acc
+	  if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc
 	  else (* No recursion on the evar instantiation *) acc
       | _         ->
 	  fold_constr collrec acc c in
@@ -103,13 +103,14 @@ let push_dependent_evars sigma emap =
   Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
     List.fold_left 
       (fun (sigma',emap') ev -> 
-	(Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev))
+	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
     
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
+  let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let change_exist evar =
     let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
@@ -117,7 +118,7 @@ let evars_to_metas sigma (emap, c) =
     mkCast (mkMeta n, DEFAULTcast, ty) in
   let rec replace c =
     match kind_of_term c with
-        Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev
+        Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev
       | _ -> map_constr replace c in
   (sigma', replace c)
 
@@ -297,7 +298,7 @@ let is_defined_equation env evd (ev,inst) rhs =
   is_pattern inst &&
   not (occur_evar ev rhs) &&
   try
-    let evi = Evd.map (evars_of evd) ev in
+    let evi = Evd.find (evars_of evd) ev in
     let (evd',body) = inverse_instance env evd ev evi inst rhs in
     evar_well_typed_body evd' ev evi body
   with Failure _ -> false
@@ -313,7 +314,7 @@ let is_defined_equation env evd (ev,inst) rhs =
 
 let do_restrict_hyps evd ev args =
   let args = Array.to_list args in
-  let evi = Evd.map (evars_of !evd) ev in
+  let evi = Evd.find (evars_of !evd) ev in
   let env = evar_env evi in
   let hyps = evar_context evi in
   let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
@@ -395,7 +396,7 @@ let evar_define env (ev,argsv) rhs isevars =
   if occur_evar ev rhs
   then error_occur_check env (evars_of isevars) ev rhs;
   let args = Array.to_list argsv in 
-  let evi = Evd.map (evars_of isevars) ev in
+  let evi = Evd.find (evars_of isevars) ev in
   (* the bindings to invert *)
   let worklist = make_subst (evar_env evi) args in
   let (isevars',body) = real_clean env isevars ev evi worklist rhs in
@@ -502,7 +503,7 @@ let status_changed lev (pbty,t1,t2) =
 
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then (isevars,[]) else
-  let evd = Evd.map (evars_of isevars) ev in
+  let evd = Evd.find (evars_of isevars) ev in
   let hyps = evar_context evd in
   let (isevars',_,rsign) = 
     array_fold_left2
@@ -599,7 +600,7 @@ let mk_valcon c = Some c
    cumulativity now includes Prop and Set in Type...
    It is, but that's not too bad *)
 let define_evar_as_abstraction abs evd (ev,args) =
-  let evi = Evd.map (evars_of evd) ev in
+  let evi = Evd.find (evars_of evd) ev in
   let evenv = evar_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) in
   let nvar =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5da0a1a999..7139956411 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -48,17 +48,16 @@ let empty = Evarmap.empty
 
 let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
 let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
-let map evc k = Evarmap.find k evc
-let rmv evc k = Evarmap.remove k evc
-let remap evc k i = Evarmap.add k i evc
-let in_dom evc k = Evarmap.mem k evc
+let find evc k = Evarmap.find k evc
+let remove evc k = Evarmap.remove k evc
+let mem evc k = Evarmap.mem k evc
 let fold = Evarmap.fold
 
 let add evd ev newinfo =  Evarmap.add ev newinfo evd
 
 let define evd ev body = 
   let oldinfo =
-    try map evd ev
+    try find evd ev
     with Not_found -> error "Evd.define: cannot define undeclared evar" in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
@@ -68,10 +67,10 @@ let define evd ev body =
     | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "Evd.define: cannot define an isevar twice"
     
-let is_evar sigma ev = in_dom sigma ev
+let is_evar sigma ev = mem sigma ev
 
 let is_defined sigma ev =
-  let info = map sigma ev in 
+  let info = find sigma ev in 
   not (info.evar_body = Evar_empty)
 
 let evar_body ev = ev.evar_body
@@ -112,7 +111,7 @@ let instantiate_evar sign c args =
 
 let existential_type sigma (n,args) =
   let info =
-    try map sigma n
+    try find sigma n
     with Not_found ->
       anomaly ("Evar "^(string_of_existential n)^" was not declared") in
   let hyps = evar_context info in
@@ -121,7 +120,7 @@ let existential_type sigma (n,args) =
 exception NotInstantiatedEvar
 
 let existential_value sigma (n,args) =
-  let info = map sigma n in
+  let info = find sigma n in
   let hyps = evar_context info in
   match evar_body info with
     | Evar_defined c ->
@@ -270,10 +269,9 @@ type evar_map = evar_map1 * sort_constraints
 let empty = empty, UniverseMap.empty
 let add (sigma,sm) k v = (add sigma k v, sm)
 let dom (sigma,_) = dom sigma
-let map (sigma,_) = map sigma
-let rmv (sigma,sm) k = (rmv sigma k, sm)
-let remap (sigma,sm) k v = (remap sigma k v, sm)
-let in_dom (sigma,_) = in_dom sigma
+let find (sigma,_) = find sigma
+let remove (sigma,sm) k = (remove sigma k, sm)
+let mem (sigma,_) = mem sigma
 let to_list (sigma,_) = to_list sigma
 let fold f (sigma,_) = fold f sigma
 let define (sigma,sm) k v = (define sigma k v, sm)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 35bcb67c70..6481ff2012 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -43,10 +43,9 @@ val empty : evar_map
 val add : evar_map -> evar -> evar_info -> evar_map
 
 val dom : evar_map -> evar list
-val map : evar_map -> evar -> evar_info
-val rmv : evar_map -> evar -> evar_map
-val remap : evar_map -> evar -> evar_info -> evar_map
-val in_dom : evar_map -> evar -> bool
+val find : evar_map -> evar -> evar_info
+val remove : evar_map -> evar -> evar_map
+val mem : evar_map -> evar -> bool
 val to_list : evar_map -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 82a45ad443..01841641cf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -273,7 +273,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | REvar (loc, ev, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-	let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
+	let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
 	let args = match instopt with
           | None -> instance_from_named_context hyps
           | Some inst -> failwith "Evar subtitutions not implemented" in
@@ -657,8 +657,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let rec proc_rec c =
       match kind_of_term c with
 	| Evar (ev,args) ->
-            assert (Evd.in_dom sigma ev);
-	    if not (Evd.in_dom initial_sigma ev) then
+            assert (Evd.mem sigma ev);
+	    if not (Evd.mem initial_sigma ev) then
               let (loc,k) = evar_source ev !isevars in
 		error_unsolvable_implicit loc env sigma k
 	| _ -> iter_constr proc_rec c
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 20b48a01ae..9a01250250 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -428,13 +428,13 @@ let whd_betadeltaiota_nolet env sigma x =
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar (ev,args)
-        when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+        when Evd.mem sigma ev & Evd.is_defined sigma ev ->
 	whd_evar sigma (Evd.existential_value sigma (ev,args))
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> collapse_appl c
 
-let nf_evar evd =
-  local_strong (whd_evar evd)
+let nf_evar sigma =
+  local_strong (whd_evar sigma)
 
 (* lazy reduction functions. The infos must be created for each term *)
 let clos_norm_flags flgs env sigma t =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c5d7d6726..f231c728b3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -259,7 +259,7 @@ let w_merge env with_types mod_delta metas evars evd =
             end
 
   and mimick_evar evd mod_delta hdc nargs sp =
-    let ev = Evd.map (evars_of evd) sp in
+    let ev = Evd.find (evars_of evd) sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =