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

8 files changed, 111 insertions, 111 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 436e8e3c39..057f342aa6 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 dd2af306c9..420cbe2900 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 c0388a383a..ee4306b7dc 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 272225acae..bc42221758 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 029616e599..704867b8d8 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 05c27cd342..d8ae031305 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 c22a160480..4347366676 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 ba8c37fb6b..8ea2eae11b 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)