Optimisation de clenv.ml pour que meta_instance ne soit pas appelé

abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.



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

9 files changed, 32 insertions, 31 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 58730d5d1b..e9ec90ec33 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_type ce in
+	let c' = clenv_direct_nf_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_type ce in
+	let c' = clenv_direct_nf_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_type ce));
+         pat = Some (Pattern.pattern_of_constr (clenv_direct_nf_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 e9bd15b119..c7cebd1108 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_type eqclause) in
+  let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_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_value eqclause);
+      { cl=eqclause; prf=(Clenv.clenv_direct_value eqclause);
 	car=ty1; rel=mkApp (equiv, Array.of_list others);
 	l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
 
@@ -808,6 +808,7 @@ 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
@@ -818,7 +819,8 @@ 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_value env', Clenv.clenv_type env') };
+		  abs = Some (Clenv.clenv_direct_value env', 
+		              Clenv.clenv_direct_nf_type env') };
 		env', prf, c1, c2, car, rel
 	  | None ->
 	      let env' =
@@ -829,6 +831,7 @@ 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
@@ -838,7 +841,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_value env') in
+	      and prf = nf (Clenv.clenv_direct_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 +1580,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' = {cl with evd = env'} in
-  let c1 = Clenv.clenv_nf_meta cl' c1 
-  and c2 = Clenv.clenv_nf_meta cl' c2 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
   check_evar_map_of_evars_defs env';
-  let prf = Clenv.clenv_value cl' in
-  let prfty = Clenv.clenv_type cl' in
+  let prf = Clenv.clenv_direct_value cl' in
+  let prfty = Clenv.clenv_direct_nf_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/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 5777d6af87..fa1a703b95 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Refiner
 open Names
@@ -23,7 +23,8 @@ val automation_tac : tactic
 
 val daimon_subtree: pftreestate -> pftreestate
 
-val concl_refiner: Termops.metamap -> constr -> Proof_type.goal sigma -> constr
+val concl_refiner: 
+  Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
 
 val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate
 val proof_instr: Decl_expr.raw_proof_instr -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9994bd7848..123c83e400 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_fchain argmv f_clause clause
+  clenv_expand_metas (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/refine.ml b/tactics/refine.ml
index 39567f9810..c0db5def58 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -60,7 +60,7 @@ open Tactics
 open Tacticals
 open Printer
 
-type term_with_holes = TH of constr * metamap * sg_proofs
+type term_with_holes = TH of constr * meta_type_map * sg_proofs
 and  sg_proofs       = (term_with_holes option) list
 
 (* pour debugger *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 644a68666a..22596ac3c0 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_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
  let rec split_last_two = function
    | [c1;c2] -> [],(c1, c2)
    | x::y::z ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c40d402086..72500c7e3d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -486,7 +486,9 @@ let rec intern_intro_pattern lf ist = function
       loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
   | loc, IntroIdentifier id ->
       loc, IntroIdentifier (intern_ident lf ist id)
-  | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)
+  | loc, IntroFresh id ->
+      loc, IntroFresh (intern_ident lf ist id)
+  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _)
       as x -> x
 
 and intern_or_and_intro_pattern lf ist =
@@ -1644,7 +1646,9 @@ let rec interp_intro_pattern ist gl = function
       loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l)
   | loc, IntroIdentifier id ->
       loc, interp_intro_pattern_var loc ist (pf_env gl) id
-  | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)
+  | loc, IntroFresh id ->
+      loc, IntroFresh (interp_fresh_ident ist gl id)
+  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _)
       as x -> x
 
 and interp_or_and_intro_pattern ist gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 02d9544f00..65082c2ee8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -560,11 +560,12 @@ 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
+  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 clenv in
+  let new_hyp_prf = clenv_value_cast_meta clenv in
   tclTHEN
     (tclEVARS (evars_of clenv.evd))
     (cut_replacing id new_hyp_typ
@@ -597,12 +598,6 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
   res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
     gl
 
-(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
- * refine fails *)
-
-let type_clenv_binding wc (c,t) lbind = 
-  clenv_type (make_clenv_binding wc (c,t) lbind)
-
 (* 
  * Elimination tactic with bindings and using an arbitrary 
  * elimination constant called elimc. This constant should end 
@@ -947,7 +942,8 @@ 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 (thd,tstack) = whd_stack (clenv_value clause) in
+      let clause = clenv_expand_metas clause in
+      let (thd,tstack) = whd_stack (clenv_direct_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m -> 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1ebaec3b4e..99f2140dd1 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -38,9 +38,6 @@ val inj_ebindings : constr bindings -> open_constr bindings
 
 (*s General functions. *)
 
-val type_clenv_binding : goal sigma ->
-  constr * constr -> open_constr bindings  -> constr
-
 val string_of_inductive : constr -> string
 val head_constr       : constr -> constr list
 val head_constr_bound : constr -> constr list -> constr list