From 9126f15c19a83a6861f6287bb60c76cd3ae5de73 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 May 2003 21:58:09 +0000
Subject: Preservation affichage des ?n en V7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pattern.ml  | 7 ++++++-
 pretyping/pattern.mli | 5 ++++-
 syntax/PPConstr.v     | 2 +-
 tactics/tauto.ml4     | 2 +-
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 0a3f6d995..93500fd54 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -21,9 +21,14 @@ open Pp
 (* Metavariables *)
 
 type patvar_map = (patvar * constr) list
-let patvar_of_int n = Names.id_of_string ("X" ^ string_of_int n)
+let patvar_of_int n =
+  let p = if !Options.v7 & not (Options.do_translate ()) then "?" else "X"
+  in
+  Names.id_of_string (p ^ string_of_int n)
 let pr_patvar = pr_id
 
+let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n)
+
 (* Patterns *)
 
 type constr_pattern =
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 535ca8c01..896cef1ff 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -22,9 +22,12 @@ open Rawterm
 (* Pattern variables *)
 
 type patvar_map = (patvar * constr) list
-val patvar_of_int : int -> patvar
 val pr_patvar : patvar -> std_ppcmds
 
+(* Only for v7 parsing/printing *)
+val patvar_of_int : int -> patvar
+val patvar_of_int_v7 : int -> patvar
+
 (* Patterns *)
 
 type constr_pattern =
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index e3ae94745..1ec635e65 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -51,7 +51,7 @@ Syntax constr
    deal with the duality CCI/FW) *)
 
   | evar [ ? ] -> ["?"]
-  | meta [ << (META $n) >> ] -> [ "?" $n ]
+  | meta [ << (META $n) >> ] -> [ $n ]
   | implicit [ << (IMPLICIT) >> ] -> ["<Implicit>"]
   | indice [ << (REL ($NUM $n)) >> ] -> ["<Unbound ref: " $n ">"]
   | instantiation [ << (INSTANCE $a ($LIST $l)) >> ] ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index bc746094a..c22195945 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -23,7 +23,7 @@ open Tactics
 open Util
 
 let assoc_last ist =
-  match List.assoc (Pattern.patvar_of_int 1) ist.lfun with
+  match List.assoc (Pattern.patvar_of_int_v7 1) ist.lfun with
     | VConstr c -> c
     | _ -> failwith "Tauto: anomaly"
 
-- 
cgit v1.2.3