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

2 files changed, 12 insertions, 7 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index bb22475230..f53f28bbba 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -19,6 +19,7 @@ open Esubst
 (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
 type existential_key = int
+type metavariable = int
 
 (* This defines Cases annotations *)
 type pattern_source = DefaultPat of int | RegularPat
@@ -71,7 +72,7 @@ type ('constr, 'types) pcofixpoint =
 type ('constr, 'types) kind_of_term =
   | Rel       of int
   | Var       of identifier
-  | Meta      of int
+  | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
   | Cast      of 'constr * 'types
@@ -120,7 +121,7 @@ type cofixpoint = int * rec_declaration
 let comp_term t1 t2 =
   match t1, t2 with
   | Rel n1, Rel n2 -> n1 = n2
-  | Meta m1, Meta m2 -> m1 = m2
+  | Meta m1, Meta m2 -> m1 == m2
   | Var id1, Var id2 -> id1 == id2
   | Sort s1, Sort s2 -> s1 == s2
   | Cast (c1,t1), Cast (c2,t2) -> c1 == c2 & t1 == t2
@@ -150,7 +151,8 @@ let comp_term t1 t2 =
 
 let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t =
   match t with
-  | Rel _ | Meta _ -> t
+  | Rel _ -> t
+  | Meta x -> Meta x
   | Var x -> Var (sh_id x)
   | Sort s -> Sort (sh_sort s)
   | Cast (c,t) -> Cast (sh_rec c, sh_rec t)
diff --git a/kernel/term.mli b/kernel/term.mli
index 2c8e9be3f0..5f3807605e 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -35,6 +35,9 @@ val family_of_sort : sorts -> sorts_family
 (*s Existential variables *)
 type existential_key = int
 
+(*s Existential variables *)
+type metavariable = int
+
 (*s Case annotation *)
 type pattern_source = DefaultPat of int | RegularPat
 type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
@@ -84,8 +87,8 @@ val mkRel : int -> constr
 (* Constructs a Variable *)
 val mkVar : identifier -> constr
 
-(* Constructs an metavariable named "?n" *)
-val mkMeta : int -> constr
+(* Constructs an patvar named "?n" *)
+val mkMeta : metavariable -> constr
 
 (* Constructs an existential variable *)
 type existential = existential_key * constr array
@@ -187,7 +190,7 @@ type ('constr, 'types) pcofixpoint =
 type ('constr, 'types) kind_of_term =
   | Rel       of int
   | Var       of identifier
-  | Meta      of int
+  | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
   | Cast      of 'constr * 'types
@@ -246,7 +249,7 @@ val is_small : sorts -> bool
 val destRel : constr -> int
 
 (* Destructs an existential variable *)
-val destMeta : constr -> int
+val destMeta : constr -> metavariable
 
 (* Destructs a variable *)
 val destVar : constr -> identifier