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

4 files changed, 18 insertions, 15 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 624b671d3..5c204c8bb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -40,28 +40,30 @@ open Clenv
 
 let clenv_cast_meta clenv = 
   let rec crec u =
-    match kind_of_term u with
+    match kind_of_term2 u with
       | App _ | Case _ -> crec_hd u
-      | Cast (c,_,_) when isMeta c -> u
+      | Cast (Meta mv,_,_) | Meta mv ->
+	  (match Evd.meta_opt_fvalue clenv.evd mv with
+	  | Some (c,_) -> c.rebus
+	  | None -> u)
       | _  -> map_constr crec u
 	    
   and crec_hd u =
     match kind_of_term (strip_outer_cast u) with
       | Meta mv ->
-	  (try 
-            let b = Typing.meta_type clenv.evd mv in
-	    if occur_meta b then u
-            else mkCast (mkMeta mv, DEFAULTcast, b)
-	  with Not_found -> u)
+	  (match Evd.find_meta clenv.evd mv with
+	  | Clval (_,(body,_),_) -> body.rebus
+	  | Cltyp (_,typ) -> 
+	      assert (not (occur_meta typ.rebus));
+	      mkCast (mkMeta mv, DEFAULTcast, typ.rebus))
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
-      | Case(ci,p,c,br) ->
-	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+      | Case(ci,p,c,br) -> mkCase (ci, crec p, crec_hd c, Array.map crec br)
       | _ -> u
   in 
   crec
 
 let clenv_value_cast_meta clenv =
-    clenv_cast_meta clenv (clenv_value clenv)
+  clenv_cast_meta clenv (clenv_direct_value clenv)
 
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent false clenv in
@@ -72,10 +74,11 @@ let clenv_pose_dependent_evars with_evars clenv =
 
 
 let clenv_refine with_evars clenv gls =
+  let clenv = clenv_expand_metas clenv in
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   tclTHEN
     (tclEVARS (evars_of clenv.evd)) 
-    (refine (clenv_cast_meta clenv (clenv_value clenv)))
+    (refine (clenv_value_cast_meta clenv))
     gls
 
 let dft = Unification.default_unify_flags
diff --git a/proofs/logic.ml b/proofs/logic.ml
index eb879d977..c358de9ba 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -251,7 +251,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   match kind_of_term trm with
     | Meta _ ->
 	if !check && occur_meta conclty then
-	  anomaly "refined called with a dependent meta";
+	  anomaly "refine called with a dependent meta";
 	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
     | Cast (t,_, ty) ->
@@ -329,7 +329,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | _ ->
 	if !check && occur_meta trm then
-	  anomaly "refined called with a dependent meta";
+	  anomaly "refine called with a dependent meta";
 	goalacc, goal_type_of env sigma trm
 
 and mk_arggoals sigma goal goalacc funty = function
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6d5f26bae..f6ebcae66 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -205,7 +205,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate
 
 val mk_pftreestate : goal -> pftreestate
 val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
 val extract_pftreestate : pftreestate -> constr
 val first_unproven : pftreestate -> pftreestate
 val last_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d9a89329a..a73e79a0c 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -106,7 +106,7 @@ val weak_undo_pftreestate   : pftreestate -> pftreestate
 val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate       : tactic -> pftreestate -> pftreestate
 val mk_pftreestate          : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
 val extract_pftreestate     : pftreestate -> constr
 val first_unproven          : pftreestate -> pftreestate
 val last_unproven           : pftreestate -> pftreestate