amelioration de la structure des univers

elimination des compteurs globaux de metas et d'evars du noyau
nettoyage de safe_typing.ml (plus de flags)


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

14 files changed, 26 insertions, 18 deletions

diff --git a/tactics/Refine.v b/tactics/Refine.v
index fb73d66ee3..4d6c117e3e 100644
--- a/tactics/Refine.v
+++ b/tactics/Refine.v
@@ -14,4 +14,4 @@ Grammar tactic simple_tactic: ast :=
   tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)].
 
 Syntax tactic level 0:
-  tcc [ (Refine $C) ] -> ["Refine " $C].
+  tcc [ <<(Tcc $C)>> ] -> ["Refine " $C].
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 721ad2cf37..30918241b1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -22,6 +22,7 @@ open Tacmach
 open Proof_type
 open Pfedit
 open Rawterm
+open Evar_refiner
 open Tacred
 open Tactics
 open Tacticals
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index a40a748435..95f8f170ea 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -229,11 +229,11 @@ let _ =
 	     add_destructor_hint na
                (match loc with
 		  | Hyp b ->
-		      Hyp(b,{d_typ=pat;d_sort=PMeta(Some (new_meta()))},
-			  { d_typ=PMeta(Some (new_meta()));
-		       	    d_sort=PMeta(Some (new_meta())) })
+		      Hyp(b,{d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))},
+			  { d_typ=PMeta(Some (Clenv.new_meta()));
+		       	    d_sort=PMeta(Some (Clenv.new_meta())) })
 		  | Concl () ->
-		      Concl({d_typ=pat;d_sort=PMeta(Some (new_meta()))}))
+		      Concl({d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))}))
                pri code
        | _ -> bad_vernac_args "HintDestruct")
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2a13a9718e..f86262b5cf 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -17,6 +17,7 @@ open Reduction
 open Proof_type
 open Proof_trees
 open Tacmach
+open Evar_refiner
 open Tactics
 open Pattern
 open Clenv
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c64a869498..6f76482931 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -23,6 +23,7 @@ open Retyping
 open Tacmach
 open Proof_type
 open Logic
+open Evar_refiner
 open Wcclausenv
 open Pattern
 open Hipattern
@@ -693,7 +694,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       let (a,p) = match whd_beta_stack ty with
 	| (_,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausale_forme: should be a sigma type" in
-      let mv = new_meta() in
+      let mv = Clenv.new_meta() in
       let rty = applist(p,[mkMeta mv]) in
       let (bindings,tuple_tail) = sigrec_clausale_forme (siglen-1) rty in
       let w =
@@ -953,7 +954,7 @@ let swapEquandsInConcl gls =
     with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) 
   in
   let sym_equal = lbeq.sym () in
-  refine (applist(sym_equal,[t;e2;e1;mkMeta (new_meta())])) gls
+  refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls
 
 let swapEquandsInHyp id gls =
   ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls)))
@@ -1012,8 +1013,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
     else
       (build_non_dependent_rewrite_predicate (t,e1,e2)  body  gls)
   in
-  refine (applist(eq_elim,[t;e1;p;mkMeta(new_meta());
-                           e2;mkMeta(new_meta())])) gls
+  refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta());
+                           e2;mkMeta(Clenv.new_meta())])) gls
 
 (* [subst_tuple_term dep_pair B]
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 57d6ca7012..65e49d1186 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -21,6 +21,7 @@ open Reduction
 open Retyping
 open Tacmach
 open Proof_type
+open Evar_refiner
 open Clenv
 open Tactics
 open Wcclausenv
@@ -368,7 +369,7 @@ let res_case_then gene thin indbinding id status gl =
            (tclTHEN (applyUsing
                        (applist(mkVar (out_some cls),
                                 list_tabulate
-                                  (fun _ -> mkMeta(new_meta())) neqns)))
+                                  (fun _ -> mkMeta(Clenv.new_meta())) neqns)))
               Auto.default_auto));
       case_tac (introCaseAssumsThen case_trailer_tac)
         (Some elim_predicate) ([],[]) newc])
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 3759093f11..39b2c7a738 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -23,13 +23,12 @@ open Tacmach
 open Proof_trees
 open Proof_type
 open Pfedit
+open Evar_refiner
 open Clenv
 open Declare
 open Wcclausenv
-(*open Pattern*)
 open Tacticals
 open Tactics
-(*open Equality*)
 open Inv
 
 let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 9492e8eb2e..aecc7fbea7 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -77,7 +77,7 @@ and pp_sg sg =
   hOV 0 (prlist_with_sep (fun _ -> [< 'fNL >])
 	   (function None -> [< 'sTR"None" >] | Some th -> [< pp_th th >]) sg)
      
-(*  compute_metamap : constr -> term_with_holes
+(*  compute_metamap : constr -> 'a evar_map -> term_with_holes
  *  réalise le 2. ci-dessus
  *
  *  Pour cela, on renvoie une metamap qui indique pour chaque meta-variable
@@ -93,7 +93,7 @@ and pp_sg sg =
 let replace_by_meta env = function
   | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
   | (TH (c,mm,_)) as th ->
-      let n = new_meta() in
+      let n = Clenv.new_meta() in
       let m = mkMeta n in
       (* quand on introduit une mv on calcule son type *)
       let ty = match kind_of_term c with
@@ -134,7 +134,6 @@ let rec compute_metamap env c = match kind_of_term c with
   | (IsConst _ | IsEvar _ | IsMutInd _ | IsMutConstruct _ |
     IsSort _ | IsVar _ | IsRel _) -> 
       TH (c,[],[])
-
   (* le terme est une mv => un but *)
   | IsMeta n ->
       (* 
@@ -278,8 +277,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 
 (* Et finalement la tactique refine elle-même : *)
 
-let refine (lmeta,c) gl =
+let refine oc gl =
   let env = pf_env gl in
+  let (_,c) = Clenv.exist_to_meta oc in
   let th = compute_metamap env c in
   tcc_aux th gl
 
diff --git a/tactics/refine.mli b/tactics/refine.mli
index f50ea12b41..ec251b8ee9 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -11,5 +11,5 @@
 open Term
 open Tacmach
 
-val refine : (int * constr) list * constr -> tactic
-val refine_tac : (int * constr) list * constr -> tactic
+val refine : Pretyping.open_constr -> tactic
+val refine_tac : Pretyping.open_constr -> tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 787413d92f..e18887fa56 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -21,6 +21,7 @@ open Declare
 open Tacmach
 open Clenv
 open Pattern
+open Evar_refiner
 open Wcclausenv
 open Pretty
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 247b9f07e9..0dea04fac9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -25,6 +25,7 @@ open Tacmach
 open Proof_trees
 open Proof_type
 open Logic
+open Evar_refiner
 open Clenv
 open Tacticals
 open Hipattern
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e17806ab76..07db3b4590 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -16,6 +16,7 @@ open Tacmach
 open Proof_type
 open Reduction
 open Evd
+open Evar_refiner
 open Clenv
 open Tacred
 open Tacticals
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 1255cad54d..3215cf017c 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -20,6 +20,7 @@ open Tacmach
 open Evd
 open Proof_trees
 open Clenv
+open Evar_refiner
 
 (* If you have a precise idea of the intended use of the following code, please
    write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index b7de77101c..8f9cad9a9d 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -16,6 +16,7 @@ open Environ
 open Evd
 open Proof_type
 open Tacmach
+open Evar_refiner
 open Clenv
 (*i*)