Uniformisation politique de nommage evd/isevars (evd si evar_defs,

evdref si evar_defs ref)


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

2 files changed, 14 insertions, 14 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4f94ba5953..7681a03a4e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -656,13 +656,13 @@ let minimal_free_rels env sigma (c,cty) =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let { intro = exist_term } = find_sigma_data sort_of_ty in 
-  let isevars = ref (Evd.create_goal_evar_defs sigma) in
+  let evdref = ref (Evd.create_goal_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
       (* is the default value typable with the expected type *)
       let dflt_typ = type_of env sigma dflt in
-      if Evarconv.e_cumul env isevars dflt_typ p_i then
-	(* the_conv_x had a side-effect on isevars *)
+      if Evarconv.e_cumul env evdref dflt_typ p_i then
+	(* the_conv_x had a side-effect on evdref *)
 	dflt
       else
 	error "Cannot solve an unification problem"
@@ -670,18 +670,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let (a,p_i_minus_1) = match whd_beta_stack p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
-      let ev = Evarutil.e_new_evar isevars env a in
+      let ev = Evarutil.e_new_evar evdref env a in
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-	Evd.existential_opt_value (Evd.evars_of !isevars) 
+	Evd.existential_opt_value (Evd.evars_of !evdref) 
 	(destEvar ev)
       with
 	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
-  Evarutil.nf_evar (Evd.evars_of !isevars) scf
+  Evarutil.nf_evar (Evd.evars_of !evdref) scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0ed4965f32..77d9c265f4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1303,17 +1303,17 @@ let solvable_by_tactic env evi (ev,args) src =
       end
   | _ -> raise Exit
 
-let solve_remaining_evars env initial_sigma evars c =
-  let isevars = ref evars in
+let solve_remaining_evars env initial_sigma evd c =
+  let evdref = ref evd in
   let rec proc_rec c =
-    match kind_of_term (Reductionops.whd_evar (evars_of !isevars) c) with
+    match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with
       | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
-            let (loc,src) = evar_source ev !isevars in
-	    let sigma = evars_of !isevars in
+            let (loc,src) = evar_source ev !evdref in
+	    let sigma = evars_of !evdref in
 	    (try 
 	      let evi = Evd.find sigma ev in
 	      let c = solvable_by_tactic env evi k src in
-	      isevars := Evd.evar_define ev c !isevars;
+	      evdref := Evd.evar_define ev c !evdref;
 	      c
 	    with Exit ->
 	      Pretype_errors.error_unsolvable_implicit loc env sigma src)
@@ -1343,8 +1343,8 @@ let interp_econstr kind ist sigma env cc =
 
 (* Interprets an open constr *)
 let interp_open_constr ccl ist sigma env cc =
-  let isevars,c = interp_gen (OfType ccl) ist sigma env cc in
-  (evars_of isevars,c)
+  let evd,c = interp_gen (OfType ccl) ist sigma env cc in
+  (evars_of evd,c)
 
 let interp_constr = interp_econstr (OfType None)