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

1 files changed, 10 insertions, 0 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 59d61a567..106369d33 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -14,8 +14,18 @@ open Names
 open Term
 open Tacmach
 open Proof_type
+open Evar_refiner
 (*i*)
 
+(* [new_meta] is a generator of unique meta variables *)
+val new_meta : unit -> int
+
+(* [exist_to_meta] generates new metavariables for each existential
+   and performs the replacement in the given constr *)
+val exist_to_meta :
+  ((existential * constr) list * constr) ->
+  ((int * constr) list * constr)
+
 (* The Type of Constructions clausale environments. *)
 
 type 'a freelisted = {