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, 15 insertions, 7 deletions

diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 3eb6e7993d..a391abf33c 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -69,8 +69,8 @@ let rec get_subterm  (depth:int) (path: int list) (constr:constr) =
    transform constr terms into abstract syntax trees.  The second argument is
    the substitution, a list of pairs linking an integer and a constr term. *)
 
-let rec map_subst (env :env) (subst:(int * Term.constr) list) = function
-  | CMeta (_,i) ->
+let rec map_subst (env :env) (subst:patvar_map) = function
+  | CPatVar (_,(_,i)) ->
       let constr = List.assoc i subst in
       extern_constr false env constr
   | x -> map_constr_expr_with_binders (map_subst env) (fun _ x -> x) subst x;;
@@ -173,7 +173,7 @@ let dad_rule_names () =
     List.map (function (s,_) -> s) !dad_rule_list;;
 
 (* this function is inspired from matches_core in pattern.ml *)
-let constrain ((n : int),(pat : constr_pattern)) sigma =
+let constrain ((n : patvar),(pat : constr_pattern)) sigma =
   if List.mem_assoc n sigma then
     if pat = (List.assoc n sigma) then sigma
     else failwith "internal"
@@ -248,7 +248,7 @@ let rec sort_list = function
     [] -> [] 
   | a::l -> add_in_list_sorting a (sort_list l);;
 
-let mk_dad_meta n = CMeta (zz,n);;
+let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));;
 let mk_rewrite lr ast =
   let b = in_gen rawwit_bool lr in
   let cb = in_gen rawwit_constr_with_bindings ((*Ctast.ct_to_ast*) ast,NoBindings) in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 31d59cab25..a011416f11 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -197,13 +197,18 @@ let tac_qualid_to_ct_ID ref =
 let loc_qualid_to_ct_ID ref =
   CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
+let int_of_meta n = int_of_string (string_of_id n)
+let is_int_meta n = try let _ = int_of_meta n in true with _ -> false
+
 let qualid_or_meta_to_ct_ID = function
   | AN qid -> tac_qualid_to_ct_ID qid
-  | MetaNum (_,n) -> CT_metac (CT_int n)
+  | MetaNum (_,n) when is_int_meta n -> CT_metac (CT_int (int_of_meta n))
+  | MetaNum _ -> xlate_error "TODO: ident meta"
 
 let ident_or_meta_to_ct_ID = function
   | AN id -> xlate_ident id
-  | MetaNum (_,n) -> CT_metac (CT_int n)
+  | MetaNum (_,n) when is_int_meta n -> CT_metac (CT_int (int_of_meta n))
+  | MetaNum _ -> xlate_error "TODO: ident meta"
 
 let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
 
@@ -347,7 +352,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CCast (_, e, t) -> 
        CT_coerce_TYPED_FORMULA_to_FORMULA
 	 (CT_typed_formula(xlate_formula e, xlate_formula t))
-   | CMeta (_, i) -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int i))
+   | CPatVar (_, (_,i)) when is_int_meta i ->
+       CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i)))
+   | CPatVar (_, _) -> xlate_error "TODO: meta as ident"
+   | CEvar (_, _) -> xlate_error "TODO: evars"
    | CCoFix (_, (_, id), lm::lmi) -> 
      let strip_mutcorec (fid, arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in