Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern

Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau


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

1 files changed, 22 insertions, 19 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 3e39fc3e6..3babd9224 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -17,19 +17,22 @@ open Proof_type
 (*i*)
 
 (* [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> int
+val new_meta : unit -> metavariable
 
 (* [exist_to_meta] generates new metavariables for each existential
    and performs the replacement in the given constr *)
 val exist_to_meta :
-  Evd.evar_map -> Pretyping.open_constr ->
-  ((int * types) list * constr)
+  Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
 
 (* The Type of Constructions clausale environments. *)
 
+module Metaset : Set.S with type elt = metavariable
+
+module Metamap : Map.S with type key = metavariable
+
 type 'a freelisted = {
   rebus : 'a;
-  freemetas : Intset.t }
+  freemetas : Metaset.t }
 
 type clbinding = 
   | Cltyp of constr freelisted
@@ -38,8 +41,8 @@ type clbinding =
 type 'a clausenv = {
   templval : constr freelisted;
   templtyp : constr freelisted;
-  namenv : identifier Intmap.t;
-  env : clbinding Intmap.t;
+  namenv : identifier Metamap.t;
+  env : clbinding Metamap.t;
   hook : 'a }
 
 type wc = named_context sigma (* for a better reading of the following *)
@@ -53,7 +56,7 @@ type wc = named_context sigma (* for a better reading of the following *)
  * [hook] is the pointer to the current walking context, for
  *        integrating existential vars and metavars. *)
 
-val collect_metas : constr -> int list
+val collect_metas : constr -> metavariable list
 val mk_clenv : 'a -> constr -> 'a clausenv
 val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
 val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
@@ -67,46 +70,46 @@ val subst_clenv : (substitution -> 'a -> 'a) ->
 
 val connect_clenv : wc -> 'a clausenv -> wc clausenv
 val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
-val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv
+val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
 val clenv_instance_term : wc clausenv -> constr -> constr
-val clenv_pose : name * int * constr -> 'a clausenv -> 'a clausenv
+val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
 val clenv_template : 'a clausenv -> constr freelisted
 val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : wc clausenv -> int -> constr
+val clenv_instance_type : wc clausenv -> metavariable -> constr
 val clenv_instance_template : wc clausenv -> constr
 val clenv_instance_template_type : wc clausenv -> constr
 val clenv_type_of : wc clausenv -> constr -> constr
-val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_bchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
 
 (* Unification with clenv *)
 type arg_bindings = (int * constr) list
 
 val unify_0 : 
   Reductionops.conv_pb -> wc -> constr -> constr 
-    -> (int * constr) list * (constr * constr) list
+    -> Termops.metamap * (constr * constr) list
 val clenv_unify : 
   bool -> Reductionops.conv_pb -> constr -> constr ->
   wc clausenv -> wc clausenv
 val clenv_match_args :
-  constr Rawterm.explicit_substitution -> wc clausenv -> wc clausenv
+  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
 val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
 
 (* Bindings *)
-val clenv_independent : wc clausenv -> int list
-val clenv_missing : 'a clausenv -> int list
+val clenv_independent : wc clausenv -> metavariable list
+val clenv_missing : 'a clausenv -> metavariable list
 val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
   constr list -> wc clausenv -> wc clausenv
 (*
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
 *)
-val clenv_lookup_name : 'a clausenv -> identifier -> int
+val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
 val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 val make_clenv_binding_apply :
-  wc -> int -> constr * constr -> types Rawterm.substitution -> wc clausenv
+  wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
 val make_clenv_binding :
-  wc -> constr * constr -> types Rawterm.substitution -> wc clausenv
+  wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
 
 (* Tactics *)
 val unify : constr -> tactic