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

18 files changed, 158 insertions, 158 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d8c4a7067..1d89306ed 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1238,7 +1238,7 @@ let interp_open_constr_patvar sigma env c =
 	)
     | _ -> map_rawconstr patvar_to_evar r in
   let raw = patvar_to_evar raw in
-  Default.understand_tcc ( !sigma) env raw
+  Default.understand_tcc !sigma env raw
 
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
@@ -1302,7 +1302,7 @@ let interp_binder sigma env na t =
   Default.understand_type sigma env t'
 
 let interp_binder_evars evdref env na t =
-  let t = intern_gen true ( !evdref) env t in
+  let t = intern_gen true !evdref env t in
   let t' = locate_if_isevar (loc_of_rawconstr t) na t in
   Default.understand_tcc_evars evdref env IsType t'
 
@@ -1349,7 +1349,7 @@ let interp_context ?(fail_anonymous=false) sigma env params =
       (Default.understand_judgment sigma) env bl
     
 let interp_context_evars ?(fail_anonymous=false) evdref env params =
-  let bl = intern_context fail_anonymous ( !evdref) env params in
+  let bl = intern_context fail_anonymous !evdref env params in
     interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
       (Default.understand_judgment_tcc evdref) env bl
     
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 436e8e3c3..057f342aa 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -358,7 +358,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
     | None -> NotInd (None,typ)
     | Some (_,(ind,_)) ->
 	inh_coerce_to_ind evdref env typ ind;
-	try try_find_ind env ( !evdref) typ realnames
+	try try_find_ind env !evdref typ realnames
 	with Not_found -> NotInd (None,typ)
 
 let find_tomatch_tycon evdref env loc = function
@@ -372,9 +372,9 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let loc = Some (loc_of_rawconstr tomatch) in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref tomatch in
-  let typ = nf_evar ( !evdref) j.uj_type in
+  let typ = nf_evar !evdref j.uj_type in
   let t =
-    try try_find_ind env ( !evdref) typ realnames
+    try try_find_ind env !evdref typ realnames
     with Not_found ->
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
   (j.uj_val,t)
@@ -409,7 +409,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   let typ,names =
     match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in
   let typ =
-    try try_find_ind pb.env ( !(pb.evdref)) typ names
+    try try_find_ind pb.env !(pb.evdref) typ names
     with Not_found -> NotInd (None,typ) in
   let tomatch = ((current,typ),deps,dep) in
   match typ with
@@ -918,7 +918,7 @@ let expand_arg tms ccl ((_,t),_,na) =
 
 let adjust_impossible_cases pb pred tomatch submat =
   if submat = [] then
-    match kind_of_term (whd_evar ( !(pb.evdref)) pred) with
+    match kind_of_term (whd_evar !(pb.evdref) pred) with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase ->
 	let default = (coq_unit_judge ()).uj_type in
 	pb.evdref := Evd.define evk default !(pb.evdref);
@@ -973,8 +973,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
   List.fold_left (expand_arg tms) ccl''' newtomatchs
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred= abstract_predicate env ( !evdref) indf current dep tms p in
-  (pred, whd_betaiota ( !evdref)
+  let pred= abstract_predicate env !evdref indf current dep tms p in
+  (pred, whd_betaiota !evdref
            (applist (pred, realargs@[current])), new_Type ())
 
 let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
@@ -1052,7 +1052,7 @@ let rec generalize_problem names pb = function
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
-  j_nf_evar ( !(pb.evdref)) j
+  j_nf_evar !(pb.evdref) j
 
 (* Building the sub-problem when all patterns are variables *)
 let shift_problem ((current,t),_,(nadep,_)) pb =
@@ -1220,7 +1220,7 @@ and compile_generalization pb d rest =
 and compile_alias pb (deppat,nondeppat,d,t) rest =
   let history = simplify_history pb.history in
   let sign, newenv, mat =
-    insert_aliases pb.env ( !(pb.evdref)) (deppat,nondeppat,d,t) pb.mat in
+    insert_aliases pb.env !(pb.evdref) (deppat,nondeppat,d,t) pb.mat in
   let n = List.length sign in
 
   (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
@@ -1391,7 +1391,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
 	  e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in
 	lift (n'-n) impossible_case_type
     | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in
-  get_judgment_of extenv ( !evdref) t
+  get_judgment_of extenv !evdref t
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index dd2af306c..420cbe290 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -127,7 +127,7 @@ let clenv_conv_leq env sigma t c bound =
   let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
   let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
   let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
-  let args = List.map (whd_evar ( evars)) args in
+  let args = List.map (whd_evar evars) args in
   check_evars env sigma evars (applist (c,args));
   args
 
@@ -248,7 +248,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
-  if isMeta (fst (whd_stack ( clenv.evd) clenv.templtyp.rebus)) then
+  if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
     clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
       (clenv_unify_meta_types ~flags:flags clenv)
   else
@@ -335,7 +335,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
       evd = 
-        evar_merge (meta_merge clenv.evd nextclenv.evd) ( clenv.evd);
+        evar_merge (meta_merge clenv.evd nextclenv.evd) clenv.evd;
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
@@ -396,7 +396,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack ( clenv.evd) u)) then
+  if isMeta (fst (whd_stack clenv.evd u)) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -410,7 +410,7 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-  let c_typ = nf_betaiota ( clenv'.evd) (clenv_get_type_of clenv' c) in
+  let c_typ = nf_betaiota clenv'.evd (clenv_get_type_of clenv' c) in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c0388a383..ee4306b7d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -43,7 +43,7 @@ module type S = sig
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
-  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  (* [inh_coerce_to_prod env evars t] coerces [t] to a product type *)
   val inh_coerce_to_prod : loc ->
     env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
 
@@ -122,7 +122,7 @@ module Default = struct
     with _ -> anomaly "apply_coercion"
 
   let inh_app_fun env evd j = 
-    let t = whd_betadeltaiota env ( evd) j.uj_type in
+    let t = whd_betadeltaiota env evd j.uj_type in
       match kind_of_term t with
 	| Prod (_,_,_) -> (evd,j)
 	| Evar ev ->
@@ -168,11 +168,11 @@ module Default = struct
     else
     let v', t' =
       try 
-	let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
+	let t2,t1,p = lookup_path_between env evd (t,c1) in
 	  match v with
 	      Some v -> 
 		let j =
-		  apply_coercion env ( evd) p
+		  apply_coercion env evd p
 		    {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
@@ -187,8 +187,8 @@ module Default = struct
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
-      kind_of_term (whd_betadeltaiota env ( evd) t),
-      kind_of_term (whd_betadeltaiota env ( evd) c1)
+      kind_of_term (whd_betadeltaiota env evd t),
+      kind_of_term (whd_betadeltaiota env evd c1)
     with
     | Prod (name,t1,t2), Prod (_,u1,u2) -> 
         (* Conversion did not work, we may succeed with a coercion. *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 272225aca..bc4222175 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -62,7 +62,7 @@ let evar_apprec env evd stack c =
   in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env evd c =
-  match kind_of_term (fst (Reductionops.whd_stack ( evd) c)) with
+  match kind_of_term (fst (Reductionops.whd_stack evd c)) with
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
@@ -166,7 +166,7 @@ let rec evar_conv_x env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then
-      if is_fconv pbty env ( evd) term1 term2 then
+      if is_fconv pbty env evd term1 term2 then
         Some true
       else if is_ground_env evd env then Some false
       else None
@@ -222,7 +222,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t2 = nf_evar ( evd) (applist appr2) in
+	    let t2 = nf_evar evd (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
 	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	  else if
@@ -254,7 +254,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t1 = nf_evar ( evd) (applist appr1) in
+	    let t1 = nf_evar evd (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
 	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	  else if
@@ -293,7 +293,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
              if the first argument is a beta-redex (expand a constant
              only if necessary) or the second argument is potentially
              usable as a canonical projection *)
-	  if isLambda flex1 or is_open_canonical_projection ( i) appr2
+	  if isLambda flex1 or is_open_canonical_projection i appr2
 	  then
 	    match eval_flexible_term env flex1 with
 	    | Some v1 ->
@@ -322,7 +322,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t2 = nf_evar ( evd) (applist appr2) in
+	  let t2 = nf_evar evd (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
 	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	else
@@ -337,7 +337,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t1 = nf_evar ( evd) (applist appr1) in
+	  let t1 = nf_evar evd (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
 	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	else
@@ -382,7 +382,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
-                 let c = nf_evar ( i) c1 in
+                 let c = nf_evar i c1 in
                  evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
 	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
@@ -390,8 +390,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               ise_and i
                 [(fun i -> evar_conv_x env i CONV b1 b2);
                  (fun i ->
-                   let b = nf_evar ( i) b1 in
-	           let t = nf_evar ( i) t1 in
+                   let b = nf_evar i b1 in
+	           let t = nf_evar i t1 in
                    evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
                  (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
@@ -414,7 +414,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
- 	         let c = nf_evar ( i) c1 in
+ 	         let c = nf_evar i c1 in
 	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
@@ -508,15 +508,15 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
 	solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
-  let evi = Evd.find ( evd) evk in
+  let evi = Evd.find evd evk in
   let subst = make_pure_subst evi args in
   let subst' = List.filter (fun (id,c) -> c = term) subst in
   if subst' = [] then error "Too complex unification problem." else
   Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta env evd (whd_castappevar ( evd) t1) in
-  let t2 = apprec_nohdbeta env evd (whd_castappevar ( evd) t2) in
+  let t1 = apprec_nohdbeta env evd (whd_castappevar evd t1) in
+  let t2 = apprec_nohdbeta env evd (whd_castappevar evd t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 029616e59..704867b8d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -79,13 +79,13 @@ let nf_evar_info evc info =
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
 
-let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars ( evd)) evd
+let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars evd) evd
 
-let nf_isevar evd = nf_evar ( evd)
-let j_nf_isevar evd = j_nf_evar ( evd)
-let jl_nf_isevar evd = jl_nf_evar ( evd)
-let jv_nf_isevar evd = jv_nf_evar ( evd)
-let tj_nf_isevar evd = tj_nf_evar ( evd)
+let nf_isevar evd = nf_evar evd
+let j_nf_isevar evd = j_nf_evar evd
+let jl_nf_isevar evd = jl_nf_evar evd
+let jv_nf_isevar evd = jv_nf_evar evd
+let tj_nf_isevar evd = tj_nf_evar evd
 
 (**********************)
 (* Creating new metas *)
@@ -322,13 +322,13 @@ let shrink_context env subst ty =
   shrink_named subst [] rev_named_sign
 
 let extend_evar env evdref k (evk1,args1) c =
-  let ty = get_type_of env ( !evdref) c in
+  let ty = get_type_of env !evdref c in
   let overwrite_first v1 v2 =
     let v = Array.copy v1 in
     let n = Array.length v - Array.length v2 in
     for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done;
     v in
-  let evi1 = Evd.find ( !evdref) evk1 in
+  let evi1 = Evd.find !evdref evk1 in
   let named_sign',rel_sign',ty =
     if k = 0 then [], [], ty
     else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in
@@ -399,7 +399,7 @@ let rec check_and_clear_in_constr evdref err ids c =
       | Evar (evk,l as ev) -> 
 	  if Evd.is_defined_evar !evdref ev then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = whd_evar ( !evdref) c in 
+	    let nc = whd_evar !evdref c in 
 	      (check_and_clear_in_constr evdref err ids nc)
 	  else 
 	    (* We check for dependencies to elements of ids in the
@@ -407,7 +407,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 	       arguments. Concurrently, we build a new evar
 	       corresponding to e where hypotheses of ids have been
 	       removed *)
-	    let evi = Evd.find ( !evdref) evk in
+	    let evi = Evd.find !evdref evk in
 	    let ctxt = Evd.evar_filtered_context evi in
 	    let (nhyps,nargs,rids) =
 	      List.fold_right2 
@@ -598,7 +598,7 @@ let rec do_projection_effects define_fun env ty evd = function
       let evd = Evd.define evk (mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = whd_betadeltaiota env ( evd) (Lazy.force ty) in
+      let ty = whd_betadeltaiota env evd (Lazy.force ty) in
       if not (isSort ty) then
 	(* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -606,7 +606,7 @@ let rec do_projection_effects define_fun env ty evd = function
            unif, we know that no coercion can be inserted) *)
 	let subst = make_pure_subst evi argsv in
 	let ty' = replace_vars subst evi.evar_concl in
-	let ty' = whd_evar ( evd) ty' in
+	let ty' = whd_evar evd ty' in
 	if isEvar ty' then define_fun env (destEvar ty') ty evd else evd
       else
 	evd
@@ -669,7 +669,7 @@ let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
 
 let instance_of_projection f env t evd projs =
-  let ty = lazy (Retyping.get_type_of env ( evd) t) in
+  let ty = lazy (Retyping.get_type_of env evd t) in
   match projs with
   | NoUniqueProjection -> raise NotUnique
   | UniqueProjection (c,effects) ->
@@ -706,7 +706,7 @@ let do_restrict_hyps_virtual evd evk filter =
        interest for this early detection in practice is not obvious. We let
        it for future work. In any case, thanks to the use of filters, the whole
        (unrestricted) context remains consistent. *)
-    let evi = Evd.find ( evd) evk in
+    let evi = Evd.find evd evk in
     let env = evar_unfiltered_env evi in
     let oldfilter = evar_filter evi in
     let filter,_ = List.fold_right (fun oldb (l,filter) ->
@@ -729,7 +729,7 @@ let do_restrict_hyps evd evk projs =
 
 let postpone_evar_term env evd (evk,argsv) rhs =
   let rhs = expand_vars_in_term env rhs in
-  let evi = Evd.find ( evd) evk in
+  let evi = Evd.find evd evk in
   let evd,evk,args =
     restrict_upon_filter evd evi evk
       (* Keep only variables that depends in rhs *)
@@ -776,7 +776,7 @@ let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) =
 exception CannotProject of projectibility_status list
 
 let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,_ as ev2) =
-  let proj1 = array_map_to_list (invert_arg env 0 ( evd) ev2) args1 in
+  let proj1 = array_map_to_list (invert_arg env 0 evd ev2) args1 in
   try
     (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *)
     let proj1' = effective_projections proj1 in
@@ -823,20 +823,20 @@ exception NotEnoughInformationToProgress
 let rec invert_definition choose env evd (evk,argsv as ev) rhs =
   let evdref = ref evd in
   let progress = ref false in
-  let evi = Evd.find ( evd) evk in
-  let subst = make_projectable_subst ( evd) evi argsv in
+  let evi = Evd.find evd evk in
+  let subst = make_projectable_subst evd evi argsv in
 
   (* Projection *)
   let project_variable t =
     (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
     try 
-      let sols = find_projectable_vars true env ( !evdref) t subst in
+      let sols = find_projectable_vars true env !evdref t subst in
       let c, p = match sols with
 	| [] -> raise Not_found
 	| [id,p] -> (mkVar id, p)
 	| (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
       in
-      let ty = lazy (Retyping.get_type_of env ( !evdref) t) in
+      let ty = lazy (Retyping.get_type_of env !evdref t) in
       let evd = do_projection_effects evar_define env ty !evdref p in
       evdref := evd;
       c
@@ -856,16 +856,16 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
 	  evar in
 
   let rec imitate (env',k as envk) t =
-    let t = whd_evar ( !evdref) t in
+    let t = whd_evar !evdref t in
     match kind_of_term t with
     | Rel i when i>k -> project_variable (mkRel (i-k))
     | Var id -> project_variable t
     | Evar (evk',args' as ev') ->
-        if evk = evk' then error_occur_check env ( evd) evk rhs;
+        if evk = evk' then error_occur_check env evd evk rhs;
 	(* Evar/Evar problem (but left evar is virtual) *)
 	let projs' =
 	  array_map_to_list
-	    (invert_arg_from_subst env k ( !evdref) subst) args'
+	    (invert_arg_from_subst env k !evdref subst) args'
 	in
 	(try
 	  (* Try to project (a restriction of) the right evar *)
@@ -894,7 +894,7 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
 	map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
 	  imitate envk t in
 
-  let rhs = whd_beta ( evd) rhs (* heuristic *) in
+  let rhs = whd_beta evd rhs (* heuristic *) in
   let body = imitate (env,0) rhs in
   (!evdref,body)
 
@@ -917,7 +917,7 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
     if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then error_occur_check env ( evd) evk body;
+    if occur_evar evk body then error_occur_check env evd evk body;
     (* needed only if an inferred type *)
     let body = refresh_universes body in
 (* Cannot strictly type instantiations since the unification algorithm
@@ -928,7 +928,7 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
       try
         let env = evar_env evi in
         let ty = evi.evar_concl in
-        Typing.check env ( evd') body ty
+        Typing.check env evd' body ty
       with e ->
         pperrnl
           (str "Ill-typed evar instantiation: " ++ fnl() ++
@@ -941,7 +941,7 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
     | NotEnoughInformationToProgress ->
 	postpone_evar_term env evd ev rhs
     | NotInvertibleUsingOurAlgorithm t -> 
-	error_not_clean env ( evd) evk t (evar_source evk evd)
+	error_not_clean env evd evk t (evar_source evk evd)
 
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
@@ -1093,7 +1093,7 @@ let status_changed lev (pbty,_,t1,t2) =
 
 let solve_refl conv_algo env evd evk argsv1 argsv2 =
   if argsv1 = argsv2 then evd else
-  let evi = Evd.find ( evd) evk in
+  let evi = Evd.find evd evk in
   (* Filter and restrict if needed *)
   let evd,evk,args =
     restrict_upon_filter evd evi evk
@@ -1113,7 +1113,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = whd_evar ( evd) t2 in
+    let t2 = whd_evar evd t2 in
     let evd = match kind_of_term t2 with
       | Evar (evk2,args2 as ev2) ->
 	  if evk1 = evk2 then
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 05c27cd34..d8ae03130 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -204,7 +204,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	for i = 0 to lt-1 do 
           if not (e_cumul env evdref (vdefj.(i)).uj_type
 		    (lift lt lar.(i))) then
-            error_ill_typed_rec_body_loc loc env ( !evdref)
+            error_ill_typed_rec_body_loc loc env !evdref
               i lna vdefj lar
 	done
 
@@ -267,7 +267,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} 
 
   let evar_kind_of_term sigma c =
-    kind_of_term (whd_evar ( sigma) c)
+    kind_of_term (whd_evar sigma c)
 
   (*************************************************************************)
   (* Main pretyping function                                               *)
@@ -299,12 +299,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | REvar (loc, evk, 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_filtered_context (Evd.find ( !evdref) evk) in
+	let hyps = evar_filtered_context (Evd.find !evdref evk) in
 	let args = match instopt with
           | None -> instance_from_named_context hyps
           | Some inst -> failwith "Evar subtitutions not implemented" in
 	let c = mkEvar (evk, args) in
-	let j = (Retyping.get_judgment_of env ( !evdref) c) in
+	let j = (Retyping.get_judgment_of env !evdref c) in
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | RPatVar (loc,(someta,n)) -> 
@@ -356,8 +356,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env evdref names ftys vdefj;
-	let ftys = Array.map (nf_evar ( !evdref)) ftys in
-	let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in
+	let ftys = Array.map (nf_evar !evdref) ftys in
+	let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
  	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -392,7 +392,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
-              let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in
+              let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
 		      let hj = pretype (mk_tycon c1) env evdref lvar c in
@@ -404,14 +404,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
 			error_cant_apply_not_functional_loc 
-			  (join_loc floc argloc) env ( !evdref)
+			  (join_loc floc argloc) env !evdref
 	      		  resj [hj]
 	in
 	let resj = apply_rec env 1 fj args in
 	let resj =
 	  match evar_kind_of_term !evdref resj.uj_val with
 	  | App (f,args) ->
-              let f = whd_evar ( !evdref) f in
+              let f = whd_evar !evdref f in
               begin match kind_of_term f with
               | Ind _ | Const _
 		  when isInd f or has_polymorphic_type (destConst f)
@@ -466,10 +466,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env ( !evdref) cj.uj_type
+	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
 	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env ( !evdref) cj 
+	      error_case_not_inductive_loc cloc env !evdref cj 
 	in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 1 then
@@ -500,7 +500,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       (Array.to_list cs.cs_concl_realargs)
 		       @[build_dependent_constructor cs] in
 		     let lp = lift cs.cs_nargs p in
-		     let fty = hnf_lam_applist env ( !evdref) lp inst in
+		     let fty = hnf_lam_applist env !evdref lp inst in
 		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
@@ -518,7 +518,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       if noccur_between 1 cs.cs_nargs ccl then
 			 lift (- cs.cs_nargs) ccl 
 		       else
-			 error_cant_find_case_type_loc loc env ( !evdref) 
+			 error_cant_find_case_type_loc loc env !evdref 
 			   cj.uj_val in
 		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
@@ -532,10 +532,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env ( !evdref) cj.uj_type
+	  try find_rectype env !evdref cj.uj_type
 	  with Not_found ->
 	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env ( !evdref) cj in
+	      error_case_not_inductive_loc cloc env !evdref cj in
 	let cstrs = get_constructors env indf in 
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
@@ -554,7 +554,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    | Some p ->
 		let env_p = push_rels psign env in
 		let pj = pretype_type empty_valcon env_p evdref lvar p in
-		let ccl = nf_evar ( !evdref) pj.utj_val in
+		let ccl = nf_evar !evdref pj.utj_val in
 		let pred = it_mkLambda_or_LetIn ccl psign in
 		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
 		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
@@ -568,8 +568,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
                       e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-	  let pred = nf_evar ( !evdref) pred in
-	  let p = nf_evar ( !evdref) p in
+	  let pred = nf_evar !evdref pred in
+	  let p = nf_evar !evdref p in
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
 	    let pi = lift n pred in (* liftn n 2 pred ? *)
@@ -624,7 +624,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RDynamic (loc,d) ->
 	if (tag d) = "constr" then
 	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env ( !evdref) c) in
+	  let j = (Retyping.get_judgment_of env !evdref c) in
 	    j
 	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
 	else
@@ -660,7 +660,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env evdref v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
+                    (loc_of_rawconstr c) env !evdref tj.utj_val v
 
   let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c22a16048..434736667 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -43,30 +43,30 @@ let inductive_type_knowing_parameters env ind jl =
 let rec execute env evd cstr =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = nf_evar ( evd) (meta_type evd n) }
+        { uj_val = cstr; uj_type = nf_evar evd (meta_type evd n) }
 
     | Evar ev ->
         let sigma =  evd in
 	let ty = Evd.existential_type sigma ev in
-	let jty = execute env evd (nf_evar ( evd) ty) in
+	let jty = execute env evd (nf_evar evd ty) in
 	let jty = assumption_of_judgment env jty in
 	{ uj_val = cstr; uj_type = jty }
 	
     | Rel n -> 
-	j_nf_evar ( evd) (judge_of_relative env n)
+	j_nf_evar evd (judge_of_relative env n)
 
     | Var id -> 
-        j_nf_evar ( evd) (judge_of_variable env id)
+        j_nf_evar evd (judge_of_variable env id)
 	  
     | Const c ->
-        make_judge cstr (nf_evar ( evd) (type_of_constant env c))
+        make_judge cstr (nf_evar evd (type_of_constant env c))
 	  
     | Ind ind ->
-	make_judge cstr (nf_evar ( evd) (type_of_inductive env ind))
+	make_judge cstr (nf_evar evd (type_of_inductive env ind))
 	  
     | Construct cstruct -> 
 	make_judge cstr
-          (nf_evar ( evd) (type_of_constructor env cstruct))
+          (nf_evar evd (type_of_constructor env cstruct))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evd c in
@@ -101,12 +101,12 @@ let rec execute env evd cstr =
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
-		    (jv_nf_evar ( evd) jl))
+		    (jv_nf_evar evd jl))
 	    | Const cst -> 
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst
-		    (jv_nf_evar ( evd) jl))
+		    (jv_nf_evar evd jl))
 	    | _ -> 
 		execute env evd f
 	in
@@ -165,13 +165,13 @@ let mcheck env evd c t =
 (* Type of a constr *)
  
 let mtype_of env evd c =
-  let j = execute env evd (nf_evar ( evd) c) in
+  let j = execute env evd (nf_evar evd c) in
   (* We are outside the kernel: we take fresh universes *)
   (* to avoid tactics and co to refresh universes themselves *)
   Termops.refresh_universes j.uj_type
 
 let msort_of env evd c =
-  let j = execute env evd (nf_evar ( evd) c) in
+  let j = execute env evd (nf_evar evd c) in
   let a = type_judgment env j in
   a.utj_type
 
@@ -185,5 +185,5 @@ let check env sigma c   =
 (* The typed type of a judgment. *)
 
 let mtype_of_type env evd constr =
-  let j = execute env evd (nf_evar ( evd) constr) in
+  let j = execute env evd (nf_evar evd constr) in
   assumption_of_judgment env j
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ba8c37fb6..8ea2eae11 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -44,14 +44,14 @@ let abstract_scheme env c l lname_typ =
     lname_typ
 
 let abstract_list_all env evd typ c l =
-  let ctxt,_ = splay_prod_n env ( evd) (List.length l) typ in
+  let ctxt,_ = splay_prod_n env evd (List.length l) typ in
   let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in 
   try 
-    if is_conv_leq env ( evd) (Typing.mtype_of env evd p) typ then p
+    if is_conv_leq env evd (Typing.mtype_of env evd p) typ then p
     else error "abstract_list_all"
   with UserError _ | Type_errors.TypeError _ ->
-    error_cannot_find_well_typed_abstraction env ( evd) p l
+    error_cannot_find_well_typed_abstraction env evd p l
 
 (**)
 
@@ -487,14 +487,14 @@ let applyHead env evd n c  =
     if n = 0 then 
       (evd, c)
     else 
-      match kind_of_term (whd_betadeltaiota env ( evd) cty) with
+      match kind_of_term (whd_betadeltaiota env evd cty) with
         | Prod (_,c1,c2) ->
             let (evd',evar) = 
 	      Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
 	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
 	| _ -> error "Apply_Head_Then"
   in 
-  apprec n c (Typing.type_of env ( evd) c) evd
+  apprec n c (Typing.type_of env evd c) evd
 
 let is_mimick_head f =
   match kind_of_term f with
@@ -524,7 +524,7 @@ let try_to_coerce env evd c cty tycon =
   let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
   let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
   if b then
-    let evd' = Evd.map_metas_fvalue (nf_evar ( evd')) evd' in
+    let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)
   else
     error "Cannot solve unification constraints"
@@ -537,7 +537,7 @@ let w_coerce_to_type env evd c cty mvty =
     (* inh_conv_coerce_rigid_to should have reasoned modulo reduction 
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
-    let cty = Tacred.hnf_constr env ( evd) cty in
+    let cty = Tacred.hnf_constr env evd cty in
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
@@ -582,7 +582,7 @@ let order_metas metas =
 
 let solve_simple_evar_eqn env evd ev rhs =
   let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
-  if not b then error_cannot_unify env ( evd) (mkEvar ev,rhs);
+  if not b then error_cannot_unify env evd (mkEvar ev,rhs);
   let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
   if not b then error "Cannot solve unification constraints";
   evd
@@ -598,7 +598,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     match evars with
     | ((evn,_ as ev),rhs)::evars' ->
     	if is_defined_evar evd ev then
-	  let v = Evd.existential_value ( evd) ev in
+	  let v = Evd.existential_value evd ev in
 	  let (evd,metas',evars'') =
 	    unify_0 env evd topconv flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
@@ -607,7 +607,7 @@ let w_merge env with_types flags (evd,metas,evars) =
           match kind_of_term rhs with
 	  | App (f,cl) when is_mimick_head f & occur_meta rhs' ->
 	      if occur_evar evn rhs' then
-                error_occur_check env ( evd) evn rhs';
+                error_occur_check env evd evn rhs';
 	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
 	      w_merge_rec evd' metas evars eqns
           | _ ->
@@ -652,7 +652,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     | [] -> evd
 		
   and mimick_evar evd flags hdc nargs sp =
-    let ev = Evd.find ( evd) sp in
+    let ev = Evd.find 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 (evd'',mc,ec) =
@@ -882,8 +882,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   w_merge env false flags (evd',[p,pred,(ConvUpToEta 0,TypeProcessed)],[])
 
 let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
-  let c1, oplist1 = whd_stack ( evd) ty1 in
-  let c2, oplist2 = whd_stack ( evd) ty2 in
+  let c1, oplist1 = whd_stack evd ty1 in
+  let c2, oplist2 = whd_stack evd ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -921,8 +921,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Meta(1) had meta-variables in it. *)
 let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
   let cv_pb = of_conv_pb cv_pb in
-  let hd1,l1 = whd_stack ( evd) ty1 in
-  let hd2,l2 = whd_stack ( evd) ty2 in
+  let hd1,l1 = whd_stack evd ty1 in
+  let hd2,l2 = whd_stack evd ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index addf12ca1..c3e6e3d87 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -80,7 +80,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
     else clenv.evd
   in
   tclTHEN
-    (tclEVARS ( evd')) 
+    (tclEVARS evd') 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1163547bf..6baedb76a 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 96cadbb02..dcb2d6037 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 ed873ce76..6da110139 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 667f5b84f..41ec5dc07 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 a87ea90ff..3cd819947 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
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2df66180c..91bf5cd21 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -65,7 +65,7 @@ type binder_list = (identifier located * bool * constr_expr) list
 (* Calls to interpretation functions. *)
 
 let interp_type_evars evdref env ?(impls=([],[])) typ =
-  let typ' = intern_gen true ~impls ( !evdref) env typ in
+  let typ' = intern_gen true ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
     
@@ -73,14 +73,14 @@ let interp_type_evars evdref env ?(impls=([],[])) typ =
 
 open Topconstr
     
-let type_ctx_instance isevars env ctx inst subst =
+let type_ctx_instance evars env ctx inst subst =
   let (s, _) = 
     List.fold_left2
       (fun (subst, instctx) (na, b, t) ce ->
 	let t' = substl subst t in
 	let c' = 
 	  match b with 
-	  | None -> interp_casted_constr_evars isevars env ce t'
+	  | None -> interp_casted_constr_evars evars env ce t'
 	  | Some b -> substl subst b
 	in
 	let d = na, Some c', t' in
@@ -126,7 +126,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
-  let isevars = ref Evd.empty in
+  let evars = ref Evd.empty in
   let tclass = 
     match bk with
     | Implicit ->
@@ -143,7 +143,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
-    let imps, c' = interp_type_evars isevars env c in
+    let imps, c' = interp_type_evars evars env c in
     let ctx, c = decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
       cl, ctx, imps, List.rev args
@@ -160,18 +160,18 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
   let env' = push_rel_context ctx' env in
-  isevars := Evarutil.nf_evar_defs !isevars;
-  isevars := resolve_typeclasses env !isevars;
-  let sigma =  !isevars in
+  evars := Evarutil.nf_evar_defs !evars;
+  evars := resolve_typeclasses env !evars;
+  let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
     if Lib.is_modtype () then
       begin
 	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype = 
 	  let t = it_mkProd_or_LetIn ty_constr ctx' in
-	    Evarutil.nf_isevar !isevars t
+	    Evarutil.nf_isevar !evars t
 	in
-	Evarutil.check_evars env Evd.empty !isevars termtype;
+	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_internal_constant id
 	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None false imps ?hook cst; id
@@ -195,7 +195,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	      let term = match props with [] -> CHole (Util.dummy_loc, None) 
 		| [(_,f)] -> f | _ -> assert false in
 	      let ty' = substl subst ty in
-	      let c = interp_casted_constr_evars isevars env' term ty' in
+	      let c = interp_casted_constr_evars evars env' term ty' in
 		c :: subst
 	  | _ ->
 	      let props, rest = 
@@ -213,7 +213,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 		if rest <> [] then 
 		  unbound_method env' k.cl_impl (fst (List.hd rest))
 		else
-		  type_ctx_instance isevars env' k.cl_props props subst
+		  type_ctx_instance evars env' k.cl_props props subst
 	in
 	let subst = List.fold_left2 
 	  (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
@@ -222,24 +222,24 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	let app, ty_constr = instance_constructor k subst in
 	let termtype = 
 	  let t = it_mkProd_or_LetIn ty_constr ctx' in
-	    Evarutil.nf_isevar !isevars t
+	    Evarutil.nf_isevar !evars t
 	in
 	let term = Termops.it_mkLambda_or_LetIn app ctx' in
-	isevars := Evarutil.nf_evar_defs !isevars;
-	let term = Evarutil.nf_isevar !isevars term in
-	let evm =  (undefined_evars !isevars) in
-	Evarutil.check_evars env Evd.empty !isevars termtype;
+	evars := Evarutil.nf_evar_defs !evars;
+	let term = Evarutil.nf_isevar !evars term in
+	let evm =  (undefined_evars !evars) in
+	Evarutil.check_evars env Evd.empty !evars termtype;
 	  if Evd.is_empty evm then
 	    declare_instance_constant k pri global imps ?hook id term termtype
 	  else begin
-	    isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
+	    evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	      Flags.silently (fun () ->
 		Command.start_proof id kind termtype 
 		  (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
 		    | _ -> assert false);
 		if props <> [] then 
-		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *)
+		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS !evars) *)
 		    (!refine_ref (evm, term));
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
@@ -269,7 +269,7 @@ let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref Evd.empty in
   let (env', fullctx), impls = interp_context_evars evars env l in
-  let fullctx = Evarutil.nf_rel_context_evar ( !evars) fullctx in
+  let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
   List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
   let ctx = try named_of_rel_context fullctx with _ -> 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 910a2526a..1ee7912f9 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -507,7 +507,7 @@ let check_all_names_different indl =
   if l <> [] then raise (InductiveError (SameNamesOverlap l))
 
 let mk_mltype_data evdref env assums arity indname =
-  let is_ml_type = is_sort env ( !evdref) arity in
+  let is_ml_type = is_sort env !evdref arity in
   (is_ml_type,indname,assums)
 
 let prepare_param = function
@@ -852,7 +852,7 @@ let interp_recursive fixkind l boxed =
     List.split (List.map (interp_fix_context evdref env) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
-  let fixtypes = List.map (nf_evar ( !evdref)) fixtypes in
+  let fixtypes = List.map (nf_evar !evdref) fixtypes in
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
@@ -871,8 +871,8 @@ let interp_recursive fixkind l boxed =
 
   (* Instantiate evars and check all are resolved *)
   let evd,_ = consider_remaining_unif_problems env_rec !evdref in
-  let fixdefs = List.map (nf_evar ( evd)) fixdefs in
-  let fixtypes = List.map (nf_evar ( evd)) fixtypes in
+  let fixdefs = List.map (nf_evar evd) fixdefs in
+  let fixtypes = List.map (nf_evar evd) fixtypes in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
   List.iter (check_evars env_rec Evd.empty evd) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 249c0439e..ef3ee5087 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -32,7 +32,7 @@ open Topconstr
 (********** definition d'un record (structure) **************)
 
 let interp_evars evdref env ?(impls=([],[])) k typ =
-  let typ' = intern_gen true ~impls ( !evdref) env typ in
+  let typ' = intern_gen true ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
 
@@ -40,11 +40,11 @@ let mk_interning_data env na impls typ =
   let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
   in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
     
-let interp_fields_evars isevars env nots l =
+let interp_fields_evars evars env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
-      let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in
-      let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in
+      let impl, t' = interp_evars evars env ~impls Pretyping.IsType t in
+      let b' = Option.map (fun x -> snd (interp_evars evars env ~impls (Pretyping.OfType (Some t')) x)) b in
       let impls = 
 	match i with
 	| Anonymous -> impls