Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 13 insertions, 6 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index 6e5de89ac7..ee5bb74774 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -23,27 +23,29 @@ let wildcard = id_of_string "_"
 let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
-let cut_ident s =
+let cut_ident skip_quote s =
   let s = string_of_id s in
   let slen = String.length s in
   (* [n'] is the position of the first non nullary digit *)
   let rec numpart n n' =
     if n = 0 then 
       failwith
-	("The string " ^ s ^ " is not an identifier: it contains only digits")
+	("The string " ^ s ^ " is not an identifier: it contains only digits or _")
     else 
       let c = Char.code (String.get s (n-1)) in
       if c = code_of_0 && n <> slen then 
 	numpart (n-1) n' 
       else if code_of_0 <= c && c <= code_of_9 then 
 	numpart (n-1) (n-1)
-      else 
+      else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+	numpart (n-1) (n-1)
+      else
 	n'
   in
   numpart slen slen
 
 let repr_ident s =
-  let numstart = cut_ident s in
+  let numstart = cut_ident false s in
   let s = string_of_id s in
   let slen = String.length s in
   if numstart = slen then 
@@ -61,6 +63,10 @@ let make_ident sa = function
       id_of_string s
   | None -> id_of_string (String.copy sa)
 
+let root_of_id id =
+  let suffixstart = cut_ident true id in
+  id_of_string (String.sub (string_of_id id) 0 suffixstart)
+
 (* Rem: semantics is a bit different, if an ident starts with toto00 then
   after successive renamings it comes to toto09, then it goes on with toto10 *)
 let lift_subscript id =
@@ -94,7 +100,7 @@ let has_subscript id =
   is_digit (id.[String.length id - 1])
 
 let forget_subscript id =
-  let numstart = cut_ident id in
+  let numstart = cut_ident false id in
   let newid = String.make (numstart+1) '0' in
   String.blit (string_of_id id) 0 newid 0 numstart;
   (id_of_string newid)
diff --git a/library/nameops.mli b/library/nameops.mli
index 8e751be091..1ae0c53032 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -17,7 +17,8 @@ val wildcard : identifier
 val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option
 
-val atompart_of_id : identifier -> string
+val atompart_of_id : identifier -> string  (* remove trailing digits *)
+val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *)
 
 val add_suffix : identifier -> string -> identifier
 val add_prefix : string -> identifier -> identifier