Jolification : tentative de supprimer les "( evd)" et associés qui

traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.


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

5 files changed, 15 insertions, 15 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1163547bf9..6baedb76af 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -408,7 +408,7 @@ let has_undefined p oevd evd =
   Evd.fold (fun ev evi has -> has ||
     (evi.evar_body = Evar_empty && p ev evi && 
 	(try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true)))
-    ( evd) false
+    evd false
 
 let rec merge_deps deps = function
   | [] -> [deps]
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 96cadbb027..dcb2d6037a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -665,7 +665,7 @@ let onEquality with_evars tac (c,lbindc) gls =
     with PatternMatchingFailure ->
       errorlabstrm "" (str"No primitive equality found.") in
   tclTHEN
-    (Refiner.tclEVARS ( eq_clause'.evd)) 
+    (Refiner.tclEVARS eq_clause'.evd) 
     (tac eq eq_clause') gls
 
 let onNegatedEquality with_evars tac gls =
@@ -796,21 +796,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       else
 	error "Cannot solve an unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack ( !evdref) p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" 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 ( !evdref) 
+	Evd.existential_opt_value !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 ( !evdref) scf
+  Evarutil.nf_evar !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/rewrite.ml4 b/tactics/rewrite.ml4
index ed873ce76e..6da1101393 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -150,7 +150,7 @@ let is_applied_setoid_relation t =
 	else (try      
 	    let evd, evar = Evarutil.new_evar Evd.empty (Global.env()) (new_Type ()) in
 	    let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in
-	      ignore(Typeclasses.resolve_one_typeclass (Global.env()) ( evd) inst);
+	      ignore(Typeclasses.resolve_one_typeclass (Global.env()) evd inst);
 	      true
 	  with _ -> false)
   | _ -> false
@@ -339,7 +339,7 @@ let unify_eqn env sigma hypinfo t =
 	  in
 	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
 	  let env' = { env' with evd = evd' } in
-	  let nf c = Evarutil.nf_evar ( evd') (Clenv.clenv_nf_meta env' c) in
+	  let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in
 	  let c1 = nf c1 and c2 = nf c2
 	  and car = nf car and rel = nf rel 
 	  and prf = nf (Clenv.clenv_value env') in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 667f5b84f8..41ec5dc07b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1430,7 +1430,7 @@ let solvable_by_tactic env evi (ev,args) src =
 let solve_remaining_evars env initial_sigma evd c =
   let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in
   let rec proc_rec c =
-    match kind_of_term (Reductionops.whd_evar ( !evdref) c) with
+    match kind_of_term (Reductionops.whd_evar !evdref c) with
       | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
             let (loc,src) = evar_source ev !evdref in
 	    let sigma =  !evdref in
@@ -1469,11 +1469,11 @@ let interp_econstr kind ist sigma env cc =
 (* Interprets an open constr *)
 let interp_open_constr ccl ist sigma env cc =
   let evd,c = interp_gen (OfType ccl) ist sigma env cc in
-  ( evd,c)
+  (evd,c)
 
 let interp_open_type ccl ist sigma env cc =
   let evd,c = interp_gen IsType ist sigma env cc in
-  ( evd,c)
+  (evd,c)
 
 let interp_constr = interp_econstr (OfType None)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a87ea90ff9..3cd8199479 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -613,7 +613,7 @@ let resolve_classes gl =
     if evd = Evd.empty then tclIDTAC gl
     else
       let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
-	(tclTHEN (tclEVARS ( evd')) tclNORMEVAR) gl
+	(tclTHEN (tclEVARS evd') tclNORMEVAR) gl
 
 (**************************)
 (*     Cut tactics        *)
@@ -662,7 +662,7 @@ let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   tclTHEN
-    (tclEVARS ( clenv.evd))
+    (tclEVARS clenv.evd)
     (cut_replacing id new_hyp_typ
       (fun x gl -> refine_no_check new_hyp_prf gl)) gl
 
@@ -1077,7 +1077,7 @@ let specialize mopt (c,lbind) g =
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let clause = clenv_unify_meta_types clause in
       let (thd,tstack) =
-        whd_stack ( clause.evd) (clenv_value clause) in
+        whd_stack clause.evd (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m -> 
@@ -1093,7 +1093,7 @@ let specialize mopt (c,lbind) g =
 	errorlabstrm "" (str "Cannot infer an instance for " ++
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
-      Some ( clause.evd), term
+      Some clause.evd, term
   in
   tclTHEN 
     (match evars with Some e -> tclEVARS e | _ -> tclIDTAC)
@@ -3282,5 +3282,5 @@ let unify ?(state=full_transparent_state) x y gl =
     in
     let evd = w_unify false (pf_env gl) Reduction.CONV 
       ~flags x y (Evd.create_evar_defs (project gl))
-    in tclEVARS ( evd) gl
+    in tclEVARS evd gl
   with _ -> tclFAIL 0 (str"Not unifiable") gl