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

8 files changed, 45 insertions, 34 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 75f8e7abc4..d23986def6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -105,7 +105,7 @@ let idopt_of_name = function
 let extern_evar loc n =
   warning
     "Existential variable turned into meta-variable during externalization";
-  CMeta (loc,n)
+  CPatVar (loc,(false,make_ident "META" (Some n)))
 
 let raw_string_of_ref = function
   | ConstRef kn -> 
@@ -193,7 +193,8 @@ let extern_app loc inctx impl f args =
     not !print_implicits_explicit_args &
     List.exists is_status_implicit impl
   then 
-    CAppExpl (loc, f, args)
+    if args = [] (* maybe caused by a hidden coercion *) then CRef f 
+    else CAppExpl (loc, f, args)
   else
     explicitize loc inctx impl (CRef f) args
 
@@ -222,7 +223,7 @@ let rec extern inctx scopes vars r =
 
   | REvar (loc,n) -> extern_evar loc n
 
-  | RMeta (loc,n) -> if !print_meta_as_hole then CHole loc else CMeta (loc,n)
+  | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
 
   | RApp (loc,f,args) ->
       let (f,args) =
@@ -411,7 +412,7 @@ let rec extern_pattern tenv vars env = function
 
   | PMeta None -> CHole loc
 
-  | PMeta (Some n) -> CMeta (loc,n)
+  | PMeta (Some n) -> CPatVar (loc,(false,n))
 
   | PApp (f,args) ->
       let (f,args) = 
@@ -430,7 +431,7 @@ let rec extern_pattern tenv vars env = function
       let args = List.map (extern_pattern tenv vars env) args in
       (* [-n] is the trick to embed a so patten into a regular application *)
       (* see constrintern.ml and g_constr.ml4 *)
-      explicitize loc false [] (CMeta (loc,-n)) args
+      explicitize loc false [] (CPatVar (loc,(true,n))) args
 
   | PProd (Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 13864febcb..8831b054b5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -94,9 +94,10 @@ let explain_internalisation_error = function
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
   | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
 
-let error_unbound_metanum loc n =
+let error_unbound_patvar loc n =
   user_err_loc
-    (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound")
+    (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
+      str " is unbound")
 
 (**********************************************************************)
 (* Dump of globalization (to be used by coqdoc)                       *)
@@ -470,15 +471,17 @@ let internalise isarity sigma env allow_soapp lvar c =
 		  Array.of_list (List.map (intern false env) cl))
     | CHole loc -> 
 	RHole (loc, QuestionMark)
-    | CMeta (loc, n) when allow_soapp = None or !interning_grammar ->
-	RMeta (loc, n)
-    | CMeta (loc, n) when n >=0 ->
+    | CPatVar (loc, n) when allow_soapp = None or !interning_grammar ->
+	RPatVar (loc, n)
+    | CPatVar (loc, (false,n as x)) ->
         if List.mem n (out_some allow_soapp) then 
-	  RMeta (loc, n)
+	  RPatVar (loc, x)
         else 
-          error_unbound_metanum loc n
-    | CMeta (loc, _) ->
+          error_unbound_patvar loc n
+    | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
+    | CEvar (loc, n) ->
+	REvar (loc, n)
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, c2) ->
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b135caf505..c052dadabf 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -19,6 +19,7 @@ open Rawterm
 open Pattern
 open Coqast
 open Topconstr
+open Termops
 (*i*)
 
 (*s Translation from front abstract syntax of term to untyped terms (rawconstr)
@@ -43,7 +44,7 @@ type ltac_env =
 (* Interprets global names, including syntactic defs and section variables *)
 val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
 val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> 
-    int list option -> ltac_sign -> constr_expr -> rawconstr
+    patvar list option -> ltac_sign -> constr_expr -> rawconstr
 
 (*s Composing the translation with typing *)
 val interp_constr        : evar_map -> env -> constr_expr -> constr
@@ -69,22 +70,22 @@ val type_judgment_of_rawconstr :
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it*)
 val interp_constr_gen     :
-  evar_map -> env -> ltac_env -> (int * constr) list -> constr_expr -> 
+  evar_map -> env -> ltac_env -> patvar_map -> constr_expr -> 
     constr option -> constr
 
 (* Interprets a constr according to two lists of instantiations (variables and
   metas), possibly casting it, and turning unresolved evar into metas*)
 val interp_openconstr_gen     :
   evar_map -> env -> ltac_env ->
-    (int * constr) list -> constr_expr -> constr option -> evar_map * constr
+    patvar_map -> constr_expr -> constr option -> evar_map * constr
 
 (* Interprets constr patterns according to a list of instantiations
   (variables)*)
-val interp_constrpattern_gen :
-  evar_map -> env -> ltac_env -> constr_expr -> int list * constr_pattern
+val interp_constrpattern_gen : evar_map -> env -> ltac_env -> constr_expr ->
+  patvar list * constr_pattern
 
 val interp_constrpattern : 
-  evar_map -> env -> constr_expr -> int list * constr_pattern
+  evar_map -> env -> constr_expr -> patvar list * constr_pattern
 
 val interp_reference : ltac_sign -> reference -> rawconstr
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index e1df0ab721..833da9e78e 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -13,6 +13,7 @@ open Names
 open Nametab
 open Rawterm
 open Topconstr
+open Term
 
 type argument_type =
   (* Basic types *)
@@ -39,7 +40,7 @@ type argument_type =
   | ExtraArgType of string
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
-type 'a or_metanum = AN of 'a | MetaNum of int located
+type 'a or_metanum = AN of 'a | MetaNum of patvar located
 type 'a and_short_name = 'a * identifier located option
 type rawconstr_and_expr = rawconstr * constr_expr option
 
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 88865f022a..8aa82ecb24 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -14,9 +14,10 @@ open Term
 open Libnames
 open Rawterm
 open Topconstr
+open Term
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
-type 'a or_metanum = AN of 'a | MetaNum of int located
+type 'a or_metanum = AN of 'a | MetaNum of patvar located
 type 'a and_short_name = 'a * identifier located option
 
 (* In globalize tactics, we need to keep the initial constr_expr to recompute*)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index deb6967339..f6f9fe60d3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -56,7 +56,7 @@ let rec unloc = function
   | RHole (_,x)  -> RHole (dummy_loc,x)
   | RRef (_,x) -> RRef (dummy_loc,x)
   | REvar (_,x) -> REvar (dummy_loc,x)
-  | RMeta (_,x) -> RMeta (dummy_loc,x)
+  | RPatVar (_,x) -> RPatVar (dummy_loc,x)
   | RDynamic (_,x) -> RDynamic (dummy_loc,x)
 
 let anonymize_if_reserved na t = match na with
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7f53f7eb21..c8f79b8c50 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -33,7 +33,7 @@ type aconstr =
   | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ASort of rawsort
   | AHole of hole_kind
-  | AMeta of int
+  | APatVar of patvar
   | ACast of aconstr * aconstr
   
 let name_app f e = function
@@ -59,7 +59,7 @@ let map_aconstr_with_binders_loc loc g f e = function
   | ACast (c,t) -> RCast (loc,f e c,f e t)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
-  | AMeta n -> RMeta (loc,n)
+  | APatVar n -> RPatVar (loc,(false,n))
   | ARef x -> RRef (loc,x)
 
 let rec subst_pat subst pat = 
@@ -122,7 +122,7 @@ let rec subst_aconstr subst raw =
 	if ro' == ro && r' == r && ra' == ra then raw else
 	  AOrderedCase (b,ro',r',ra')
 
-  | AMeta _ | ASort _ -> raw
+  | APatVar _ | ASort _ -> raw
 
   | AHole (ImplicitArg (ref,i)) ->
       let ref' = subst_global subst ref in 
@@ -162,7 +162,7 @@ let aconstr_of_rawconstr vars a =
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
   | RRef (_,r) -> ARef r
-  | RMeta (_,n) -> AMeta n
+  | RPatVar (_,(_,n)) -> APatVar n
   | RDynamic _ | RRec _ | REvar _ ->
       error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
 allowed in abbreviatable expressions"
@@ -198,7 +198,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
   | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
-  | RMeta (_,n1), AMeta n2 when n1=n2 -> sigma
+  | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
   | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
       List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
   | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
@@ -217,7 +217,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RCast(_,c1,t1), ACast(c2,t2) ->
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
-  | RMeta _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
+  | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, AHole _ when not(Options.do_translate()) -> sigma
   | RHole _, AHole _ -> sigma
   | (RDynamic _ | RRec _ | REvar _), _ 
@@ -285,7 +285,8 @@ type constr_expr =
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
   | CHole of loc
-  | CMeta of loc * int
+  | CPatVar of loc * (bool * patvar)
+  | CEvar of loc * existential_key
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr
   | CNotation of loc * notation * constr_expr list
@@ -321,7 +322,8 @@ let constr_loc = function
   | CCases (loc,_,_,_) -> loc
   | COrderedCase (loc,_,_,_,_) -> loc
   | CHole loc -> loc
-  | CMeta (loc,_) -> loc
+  | CPatVar (loc,_) -> loc
+  | CEvar (loc,_) -> loc
   | CSort (loc,_) -> loc
   | CCast (loc,_,_) -> loc
   | CNotation (loc,_,_) -> loc
@@ -354,7 +356,7 @@ let rec occur_var_constr_expr id = function
   | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
   | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
   | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
-  | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false
   | CCases (loc,_,_,_) 
   | COrderedCase (loc,_,_,_,_) 
   | CFix (loc,_,_) 
@@ -396,7 +398,8 @@ let map_constr_expr_with_binders f g e = function
   | CCast (loc,a,b) -> CCast (loc,f e a,f e b)
   | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
-  | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ 
+  | CNumeral _ | CDynamic _ | CRef _ as x -> x
   | CCases (loc,po,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 5c452b870b..8f0f5fb752 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -34,7 +34,7 @@ type aconstr =
   | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ASort of rawsort
   | AHole of hole_kind
-  | AMeta of int
+  | APatVar of patvar
   | ACast of aconstr * aconstr
 
 val map_aconstr_with_binders_loc : loc -> 
@@ -83,7 +83,8 @@ type constr_expr =
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
   | CHole of loc
-  | CMeta of loc * int
+  | CPatVar of loc * (bool * patvar)
+  | CEvar of loc * existential_key
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr
   | CNotation of loc * notation * constr_expr list