Avoid unnecessary normalizations w.r.t. evars in Program.

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

2 files changed, 10 insertions, 17 deletions

diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 7e57c51aea..83555716d6 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -110,7 +110,6 @@ module Coercion = struct
   and coerce loc env isevars (x : Term.constr) (y : Term.constr)
       : (Term.constr -> Term.constr) option
       =
-    let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
     let rec coerce_unify env x y =
       let x = hnf env isevars x and y = hnf env isevars y in
 	try
@@ -383,7 +382,7 @@ module Coercion = struct
     try
       let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
       let j1 = apply_coercion env ( isevars) p j t in
-	(isevars,type_judgment env (j_nf_evar ( isevars) j1))
+	(isevars, type_judgment env (j_nf_evar ( isevars) j1))
     with Not_found ->
       error_not_a_type_loc loc env ( isevars) j
 
@@ -467,8 +466,7 @@ module Coercion = struct
 	  let (evd', val') =
 	    try
 	      inh_conv_coerce_to_fail loc env evd rigidonly
-		(Some (nf_evar evd cj.uj_val))
-		(nf_evar evd cj.uj_type) (nf_evar evd t)
+		(Some cj.uj_val) cj.uj_type t
 	    with NoCoercion ->
 	      let sigma =  evd in
 		try
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index d5d427c7a6..ca5145d735 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -88,7 +88,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env evdref j = function
-    | None -> j_nf_evar !evdref j
+    | None -> j
     | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
 
   let push_rels vars env = List.fold_right push_rel vars env
@@ -340,13 +340,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
 		      let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
 		      evdref := evd;
-		      let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in
+		      let hj = pretype (mk_tycon c1) env evdref lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
-		      let typ' = nf_evar !evdref typ in
 			apply_rec env (n+1)
-			  { uj_val = nf_evar !evdref value;
-			    uj_type = nf_evar !evdref typ' }
-			  (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest
+			{ uj_val = value;
+			  uj_type = typ }
+			  (Option.map (fun (abs, c) -> abs, c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
@@ -354,9 +353,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env !evdref
 	      		  resj [hj]
 	in
-	let resj = j_nf_evar !evdref (apply_rec env 1 fj ftycon args) in
+	let resj = apply_rec env 1 fj ftycon args in
 	let resj =
-	  match kind_of_term resj.uj_val with
+	  match kind_of_term (whd_evar !evdref resj.uj_val) with
 	  | App (f,args) when isInd f or isConst f ->
 	      let sigma =  !evdref in
 	      let c = mkApp (f,Array.map (whd_evar sigma) args) in
@@ -508,10 +507,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  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
-	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
-	    let pi = lift n pred in (* liftn n 2 pred ? *)
+	    let pi = lift n pred in
 	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
 	    let csgn =
 	      if not !allow_anonymous_refs then
@@ -525,7 +523,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		cs.cs_args
 	    in
 	    let env_c = push_rels csgn env in
-(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
 	    let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	  let b1 = f cstrs.(0) b1 in
@@ -551,8 +548,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env evdref lvar t in
 		let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
-		  (* User Casts are for helping pretyping, experimentally not to be kept*)
-		  (* ... except for Correctness *)
 		let v = mkCast (cj.uj_val, k, tj.utj_val) in
 		  { uj_val = v; uj_type = tj.utj_val }
 	in