From 9126f15c19a83a6861f6287bb60c76cd3ae5de73 Mon Sep 17 00:00:00 2001
From: herbelin
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 ++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 0a3f6d995a..93500fd546 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 535ca8c01d..896cef1ff4 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 =
-- 
cgit v1.2.3