eradication de Evarutil.w_Define

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

4 files changed, 31 insertions, 35 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 759157b30..746d2cd8e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -318,6 +318,30 @@ let real_clean env isevars ev evi args rhs =
   then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd);
   (!evd,body)
 
+(* [typed_evar_define evd sp c] (tactic style)
+ *
+ * Defines evar [sp] with term [c] in evar context [evd].
+ * [c] is typed in the context of [sp] and evar context [evd] with
+ * [sp] removed to avoid circular definitions.
+ * No unification is performed in order to assert that [c] has the
+ * correct type.
+ *
+let typed_evar_define sp c evd =
+  let sigma = evars_of evd in
+  let spdecl = Evd.map sigma sp in
+  let env = evar_env spdecl in
+  let _ =
+    (* Do not consider the metamap because evars may not depend on metas *)
+    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
+    with
+	Not_found -> error "Instantiation contains unlegal variables"
+      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
+      errorlabstrm "typed_evar_define"
+      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
+       str (string_of_existential sp)) in
+  Evd.evar_define sp c evd
+*)
+
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
  * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args)
  * ?sp [ sp.hyps \ args ]  unifies to rhs
@@ -349,33 +373,6 @@ let evar_define env (ev,argsv) rhs isevars =
    let isevars'' = Evd.evar_define ev body isevars' in
    isevars'',[ev]
 
-(* [w_Define evd sp c] (tactic style)
- *
- * Defines evar [sp] with term [c] in evar context [evd].
- * [c] is typed in the context of [sp] and evar context [evd] with
- * [sp] removed to avoid circular definitions.
- * No unification is performed in order to assert that [c] has the
- * correct type.
- *)
-let w_Define sp c evd =
-  let sigma = evars_of evd in
-  if not (Evd.in_dom sigma sp) then
-    error "w_Define: cannot define undeclared evar";
-  if Evd.is_defined sigma sp then
-    error "w_Define: cannot define evar twice";
-  let spdecl = Evd.map sigma sp in
-  let env = evar_env spdecl in
-  let _ =
-    (* Do not consider the metamap because evars may not depend on metas *)
-    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
-    with
-	Not_found -> error "Instantiation contains unlegal variables"
-      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
-      errorlabstrm "w_Define"
-      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
-       str (string_of_existential sp)) in
-  let spdecl' = { spdecl with evar_body = Evar_defined c } in
-  evars_reset_evd (Evd.add sigma sp spdecl') evd
 
 
 (*-------------------*)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index e8669e5fa..11965812d 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -51,8 +51,6 @@ val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
 (***********************************************************)
 (* Instanciate evars *)
 
-val w_Define : evar -> constr -> evar_defs -> evar_defs
-
 (* suspicious env ? *)
 val evar_define :
   env -> existential -> constr -> evar_defs -> evar_defs * evar list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index dbcfae0e8..d1d8d3817 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -49,15 +49,16 @@ let fold = Evarmap.fold
 let add evd ev newinfo =  Evarmap.add ev newinfo evd
 
 let define evd ev body = 
-  let oldinfo = map evd ev in
+  let oldinfo =
+    try map evd ev
+    with Not_found -> error "Evd.define: cannot define undeclared evar" in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
       evar_hyps = oldinfo.evar_hyps;
-      evar_body = Evar_defined body} 
-  in
+      evar_body = Evar_defined body} in
   match oldinfo.evar_body with
     | Evar_empty -> Evarmap.add ev newinfo evd
-    | _ -> anomaly "cannot define an isevar twice"
+    | _ -> anomaly "Evd.define: cannot define an isevar twice"
     
 let is_evar sigma ev = in_dom sigma ev
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2801d3ee4..0c5d7d672 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -267,8 +267,8 @@ let w_merge env with_types mod_delta metas evars evd =
         (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
     let evd'' = w_merge_rec evd' mc ec in
     if (evars_of evd') == (evars_of evd'')
-    then w_Define sp c evd''
-    else w_Define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
+    then Evd.evar_define sp c evd''
+    else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
 
   (* merge constraints *)
   let evd' = w_merge_rec evd metas evars in