Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui

s'est avéré ralentir la compilation des user-contribs au final, sans
compter aussi le bug 1980 apparemment introduit par ce commit).



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

5 files changed, 16 insertions, 21 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 42d74f9ed..aa7ce1290 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -264,7 +264,7 @@ let make_exact_entry pri (c,cty) =
 	failwith "make_exact_entry"
     | _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
-	let c' = clenv_direct_nf_type ce in
+	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
 	(Some (head_of_constr_reference (List.hd (head_constr cty))),
 	   { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
@@ -274,7 +274,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
     match kind_of_term cty with
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
-	let c' = clenv_direct_nf_type ce in
+	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry") in
@@ -342,7 +342,7 @@ let make_trivial env sigma c =
   let hd = head_of_constr_reference (List.hd (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
-         pat = Some (Pattern.pattern_of_constr (clenv_direct_nf_type ce));
+         pat = Some (Pattern.pattern_of_constr (clenv_type ce));
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
 open Vernacexpr
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1ae1196a3..bda1fabbc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -751,7 +751,7 @@ let evd_convertible env evd x y =
 let decompose_setoid_eqhyp env sigma c left2right =
   let ctype = Typing.type_of env sigma c in
   let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
-  let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
+  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
     | x::y::z ->
@@ -764,7 +764,7 @@ let decompose_setoid_eqhyp env sigma c left2right =
     if not (evd_convertible env eqclause.evd ty1 ty2) then
       error "The term does not end with an applied homogeneous relation."
     else
-      { cl=eqclause; prf=(Clenv.clenv_direct_value eqclause);
+      { cl=eqclause; prf=(Clenv.clenv_value eqclause);
 	car=ty1; rel=mkApp (equiv, Array.of_list others);
 	l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
 
@@ -808,7 +808,6 @@ let unify_eqn env sigma hypinfo t =
 		cl, prf, c1, c2, car, rel
 	      else raise Not_found*)
 	      let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in
-	      let env' = clenv_expand_metas env' in
 	      let env' =
 		let mvs = clenv_dependent false env' in
 		  clenv_pose_metas_as_evars env' mvs
@@ -819,8 +818,7 @@ let unify_eqn env sigma hypinfo t =
 	      and rel = Clenv.clenv_nf_meta env' rel in
 		hypinfo := { !hypinfo with
 		  cl = env';
-		  abs = Some (Clenv.clenv_direct_value env', 
-		              Clenv.clenv_direct_nf_type env') };
+		  abs = Some (Clenv.clenv_value env', Clenv.clenv_type env') };
 		env', prf, c1, c2, car, rel
 	  | None ->
 	      let env' =
@@ -831,7 +829,6 @@ let unify_eqn env sigma hypinfo t =
 		  clenv_unify allowK ~flags:rewrite2_unif_flags
 		    CONV left t cl
 	      in
-	      let env' = clenv_expand_metas env' in
 	      let env' = 
 		let mvs = clenv_dependent false env' in
 		  clenv_pose_metas_as_evars env' mvs
@@ -841,7 +838,7 @@ let unify_eqn env sigma hypinfo t =
 	      let nf c = Evarutil.nf_evar (Evd.evars_of 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_direct_value env') in
+	      and prf = nf (Clenv.clenv_value env') in
 	      let ty1 = Typing.mtype_of env'.env env'.evd c1 
 	      and ty2 = Typing.mtype_of env'.env env'.evd c2
 	      in
@@ -1577,12 +1574,12 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
 	  Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags
 	    (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
   in
-  let cl' = clenv_expand_metas {cl with evd = env'} in
-  let c1 = Clenv.clenv_direct_nf_meta cl' c1 
-  and c2 = Clenv.clenv_direct_nf_meta cl' c2 in
+  let cl' = {cl with evd = env'} in
+  let c1 = Clenv.clenv_nf_meta cl' c1 
+  and c2 = Clenv.clenv_nf_meta cl' c2 in
   check_evar_map_of_evars_defs env';
-  let prf = Clenv.clenv_direct_value cl' in
-  let prfty = Clenv.clenv_direct_nf_type cl' in
+  let prf = Clenv.clenv_value cl' in
+  let prfty = Clenv.clenv_type cl' in
   let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 123c83e40..9994bd784 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -565,7 +565,7 @@ let apply_on_clause (f,t) clause =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
-  clenv_expand_metas (clenv_fchain argmv f_clause clause)
+  clenv_fchain argmv f_clause clause
 
 let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 22596ac3c..644a68666 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1815,7 +1815,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
 let analyse_hypothesis gl c =
  let ctype = pf_type_of gl c in
  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
  let rec split_last_two = function
    | [c1;c2] -> [],(c1, c2)
    | x::y::z ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index be15311b9..87ef65d7c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -560,12 +560,11 @@ let error_uninstantiated_metas t clenv =
   in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 let clenv_refine_in with_evars id clenv gl =
-  let clenv = clenv_expand_metas clenv in
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let new_hyp_typ = clenv_type clenv in
   if not with_evars & occur_meta new_hyp_typ then 
     error_uninstantiated_metas new_hyp_typ clenv;
-  let new_hyp_prf = clenv_value_cast_meta clenv in
+  let new_hyp_prf = clenv_value clenv in
   tclTHEN
     (tclEVARS (evars_of clenv.evd))
     (cut_replacing id new_hyp_typ
@@ -960,8 +959,7 @@ let specialize mopt (c,lbind) g =
     else 
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let clause = clenv_unify_meta_types clause in
-      let clause = clenv_expand_metas clause in
-      let (thd,tstack) = whd_stack (clenv_direct_value clause) in
+      let (thd,tstack) = whd_stack (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m ->