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

1 files changed, 20 insertions, 20 deletions

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