meilleure presentation des commentaires du traducteur

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

11 files changed, 113 insertions, 107 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index 869f55bb0..c0120177d 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -229,7 +229,7 @@ let coerce_to_id_ast a = match coerce_to_var a with
          str"This expression should be a simple identifier")
 
 let coerce_to_id = function
-  | CRef (Ident (_,id)) -> id
+  | CRef (Ident (loc,id)) -> (loc,id)
   | a -> user_err_loc
         (constr_loc a,"Ast.coerce_to_id",
          str"This expression should be a simple identifier")
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 1faaf78a7..265674a6c 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -86,7 +86,7 @@ type grammar_action =
 
 type env = (string * typed_ast) list
 
-val coerce_to_id : constr_expr -> identifier
+val coerce_to_id : constr_expr -> identifier located
 
 val coerce_global_to_id : reference -> identifier
 val coerce_reference_to_id : reference -> identifier
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index da16be9b5..bd505088c 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -28,6 +28,8 @@ let _ =
     List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
+let lstring = Gram.Entry.create "lstring"
+
 
 if !Options.v7 then
 GEXTEND Gram
@@ -42,8 +44,11 @@ END;
 
 if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: command;
+  GLOBAL: command lstring;
 
+  lstring:
+    [ [ s = STRING -> s ] ]
+  ;
   comment:
     [ [ c = constr -> CommentConstr c
       | s = STRING -> CommentString s
@@ -55,7 +60,7 @@ GEXTEND Gram
       (* System directory *)
       | IDENT "Pwd" -> VernacChdir None
       | IDENT "Cd" -> VernacChdir None
-      | IDENT "Cd"; dir = STRING -> VernacChdir (Some dir)
+      | IDENT "Cd"; dir = lstring -> VernacChdir (Some dir)
 
       (* Toplevel control *)
       | IDENT "Drop" -> VernacToplevelControl Drop
@@ -63,25 +68,25 @@ GEXTEND Gram
       | "Quit" -> VernacToplevelControl Quit
 
       (* Dump of the universe graph - to file or to stdout *) 
-      | IDENT "Dump"; IDENT "Universes"; fopt = OPT STRING ->
+      | IDENT "Dump"; IDENT "Universes"; fopt = OPT lstring ->
 	  VernacPrint (PrintUniverses fopt)
 
       | IDENT "Locate"; l = locatable -> VernacLocate l
 
       (* Managing load paths *)
-      | IDENT "Add"; IDENT "LoadPath"; dir = STRING; alias = as_dirpath ->
+      | IDENT "Add"; IDENT "LoadPath"; dir = lstring; alias = as_dirpath ->
 	  VernacAddLoadPath (false, dir, alias)
-      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = STRING; 
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = lstring; 
 	  alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
-      | IDENT "Remove"; IDENT "LoadPath"; dir = STRING ->
+      | IDENT "Remove"; IDENT "LoadPath"; dir = lstring ->
 	  VernacRemoveLoadPath dir
 
        (* For compatibility *)
-      | IDENT "AddPath"; dir = STRING; "as"; alias = as_dirpath ->
+      | IDENT "AddPath"; dir = lstring; "as"; alias = as_dirpath ->
 	  VernacAddLoadPath (false, dir, alias)
-      | IDENT "AddRecPath"; dir = STRING; "as"; alias = as_dirpath ->
+      | IDENT "AddRecPath"; dir = lstring; "as"; alias = as_dirpath ->
 	  VernacAddLoadPath (true, dir, alias)
-      | IDENT "DelPath"; dir = STRING ->
+      | IDENT "DelPath"; dir = lstring ->
 	  VernacRemoveLoadPath dir
 
       (* Printing (careful factorization of entries) *)
@@ -104,7 +109,7 @@ GEXTEND Gram
 	  VernacSearch (SearchRewrite c, l)
       | IDENT "SearchAbout"; 
 	  sl = [ "["; l = LIST1 [ r = global -> SearchRef r
-                                  | s = STRING -> SearchString s ]; "]" -> l 
+                                  | s = lstring -> SearchString s ]; "]" -> l 
    		 | qid = global -> [SearchRef qid] ];
 	  l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout sl, l)
@@ -116,9 +121,9 @@ GEXTEND Gram
 	  VernacCheckMayEval (None, None, c)
       | "Type"; c = constr -> VernacGlobalCheck c      (* pas dans le RefMan *)
 
-      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
+      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = lstring ->
 	  VernacAddMLPath (false, dir)
-      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = STRING ->
+      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = lstring ->
 	  VernacAddMLPath (true, dir)
 (*
       | IDENT "SearchIsos"; c = constr -> VernacSearch (SearchIsos c)
@@ -199,17 +204,17 @@ GEXTEND Gram
   ;
   locatable:
     [ [ qid = global -> LocateTerm qid
-      | IDENT "File"; f = STRING -> LocateFile f
+      | IDENT "File"; f = lstring -> LocateFile f
       | IDENT "Library"; qid = global -> LocateLibrary  qid
-      | s = STRING -> LocateNotation s ] ]
+      | s = lstring -> LocateNotation s ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue n
-      | s  = STRING    -> StringValue s ] ]
+      | s  = lstring    -> StringValue s ] ]
   ;
   option_ref_value:
     [ [ id = global   -> QualidRefValue id
-      | s  = STRING   -> StringRefValue s ] ]
+      | s  = lstring   -> StringRefValue s ] ]
   ;
   as_dirpath:
     [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
@@ -242,7 +247,7 @@ GEXTEND Gram
         set_default_action_parser (parser_type_from_name univ); univ ] ]
   ;
   syntax:
-   [ [ IDENT "Token"; s = STRING ->
+   [ [ IDENT "Token"; s = lstring ->
        Pp.warning "Token declarations are now useless"; VernacNop
 
      | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
@@ -257,11 +262,11 @@ GEXTEND Gram
      | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
-     | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; 
+     | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = lstring; 
 	 modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
          (s8,mv8) =
              [IDENT "V8only";
-              s8=OPT STRING;
+              s8=OPT lstring;
               mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
                 (s8,mv8)
              | -> (None,None)] ->
@@ -271,7 +276,7 @@ GEXTEND Gram
                  | _ -> List.map map_modl modl in
 	       VernacSyntaxExtension (local,Some (s,modl),Some(s8,mv8))
 
-     | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = STRING; 
+     | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = lstring; 
 	 modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   VernacSyntaxExtension (local,None,Some(s,modl))
 
@@ -291,7 +296,7 @@ GEXTEND Gram
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
      | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural;
-         op = STRING; 
+         op = lstring; 
          p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc];
@@ -299,7 +304,7 @@ GEXTEND Gram
               [IDENT "V8only";
                a8=entry_prec;
                n8=OPT natural;
-	       op8=OPT STRING;
+	       op8=OPT lstring;
                mv8=["("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> []]
 		->
 		 (match (a8,n8,mv8,op8) with
@@ -325,7 +330,7 @@ GEXTEND Gram
 		  (op8,mv8)) mv8 in
 		VernacInfix (local,(op,mv),p,v8,sc)
      | IDENT "Distfix"; local = locality; a = entry_prec; n = natural; 
-	   s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
+	   s = lstring; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
              let (a,s,c) = Metasyntax.translate_distfix a s p in
 	     let mv = Some(s,[SetLevel n;SetAssoc a]) in
              VernacNotation (local,c,mv,mv,sc)
@@ -336,12 +341,12 @@ GEXTEND Gram
 	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
 	       | -> [] ] ->
 	 VernacNotation (local,c,Some("'"^s^"'",l),None,None)
-     | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
+     | IDENT "Notation"; local = locality; s = lstring; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ];
          (s8,mv8) =
              [IDENT "V8only";
-              s8=OPT STRING;
+              s8=OPT lstring;
               mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
 		(s8,mv8)
              | -> (* Means: rules are based on V7 rules *)
@@ -353,12 +358,12 @@ GEXTEND Gram
 		 | None, Some mv8 -> Some (s,mv8) (* s like v7 *)
 		 | Some s8, Some mv8 -> Some (s8,mv8) in
                VernacNotation (local,c,Some(s,modl),smv8,sc)
-     | IDENT "V8Notation"; local = locality; s = STRING; ":="; c = constr;
+     | IDENT "V8Notation"; local = locality; s = lstring; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacNotation (local,c,None,Some(s,modl),sc)
 
-     | IDENT "V8Infix"; local = locality; op8 = STRING; p = global;
+     | IDENT "V8Infix"; local = locality; op8 = lstring; p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc] ->
            let mv8 = Metasyntax.merge_modifiers None None modl in
@@ -385,7 +390,7 @@ GEXTEND Gram
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
       | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
-      | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
+      | IDENT "format"; s = [s = lstring -> (loc,s)] -> SetFormat s ] ]
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
@@ -409,7 +414,7 @@ GEXTEND Gram
      | -> None ]]
   ;
   grammar_tactic_rule:
-    [[ name = rule_name; "["; s = STRING; pil = LIST0 production_item; "]";
+    [[ name = rule_name; "["; s = lstring; pil = LIST0 production_item; "]";
        "->"; "["; t = Tactic.tactic; "]"  -> (name, (s,pil), t) ]]
   ;
   grammar_rule:
@@ -420,7 +425,7 @@ GEXTEND Gram
     [[ name = IDENT -> name ]]
   ;
   production_item:
-    [[ s = STRING -> VTerm s
+    [[ s = lstring -> VTerm s
      | nt = non_terminal; po = OPT [ "("; p = METAIDENT; ")" -> p ] ->
          match po with
            | Some p -> VNonTerm (loc,nt,Some (Names.id_of_string p))
@@ -452,7 +457,7 @@ GEXTEND Gram
   next_hunks:
     [ [ IDENT "FNL" -> UNP_FNL
       | IDENT "TAB" -> UNP_TAB
-      | c = STRING -> RO c
+      | c = lstring -> RO c
       | "[";
         x =
           [ b = box; ll = LIST0 next_hunks -> UNP_BOX (b,ll)
@@ -478,7 +483,7 @@ GEXTEND Gram
   paren_reln_or_extern:
     [ [ IDENT "L" -> None, L
       | IDENT "E" -> None, E
-      | pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] ->
+      | pprim = lstring; precrec = OPT [ ":"; p = precedence -> p ] ->
 	  match precrec with
 	    | Some p -> Some pprim, Prec p
             | None -> Some pprim, Any ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 51480a956..1e57506df 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -92,7 +92,7 @@ GEXTEND Gram
   ;
   match_pattern:
     [ [ id = Constr.constr_pattern; "["; pc = Constr.constr_pattern; "]" ->
-        let s = coerce_to_id id in Subterm (Some s, pc)
+        let (_,s) = coerce_to_id id in Subterm (Some s, pc)
       | "["; pc = Constr.constr_pattern; "]" -> Subterm (None,pc)
       | pc = Constr.constr_pattern -> Term pc ] ]
   ;
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4
index 7e2532c20..b3a281b64 100644
--- a/parsing/g_module.ml4
+++ b/parsing/g_module.ml4
@@ -31,9 +31,9 @@ GEXTEND Gram
   ;
 
   with_declaration:
-    [ [ "Definition"; id = base_ident; ":="; c = Constr.constr ->
+    [ [ "Definition"; id = identref; ":="; c = Constr.constr ->
           CWith_Definition (id,c)
-      | IDENT "Module"; id = base_ident; ":="; qid = qualid ->
+      | IDENT "Module"; id = identref; ":="; qid = qualid ->
 	  CWith_Module (id,qid)
       ] ]
   ;
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 638591460..b011c8f33 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -45,11 +45,11 @@ GEXTEND Gram
       | "Qed" -> VernacEndProof (Proved (true,None))
       | IDENT "Save" -> VernacEndProof (Proved (true,None))
       | IDENT "Defined" -> VernacEndProof (Proved (false,None))
-      |	IDENT "Defined"; id=base_ident -> 
+      |	IDENT "Defined"; id=identref -> 
 	  VernacEndProof (Proved (false,Some (id,None)))
-      | IDENT "Save"; tok = thm_token; id = base_ident ->
+      | IDENT "Save"; tok = thm_token; id = identref ->
 	  VernacEndProof (Proved (true,Some (id,Some tok)))
-      | IDENT "Save"; id = base_ident ->
+      | IDENT "Save"; id = identref ->
 	  VernacEndProof (Proved (true,Some (id,None)))
       | IDENT "Suspend" -> VernacSuspend
       | IDENT "Resume" -> VernacResume None
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index 7d75cf4cb..28bf29b0e 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -46,12 +46,12 @@ GEXTEND Gram
       | IDENT "Admitted" -> VernacEndProof Admitted
       | IDENT "Qed" -> VernacEndProof (Proved (true,None))
       | IDENT "Save" -> VernacEndProof (Proved (true,None))
-      | IDENT "Save"; tok = thm_token; id = base_ident ->
+      | IDENT "Save"; tok = thm_token; id = identref ->
 	  VernacEndProof (Proved (true,Some (id,Some tok)))
-      | IDENT "Save"; id = base_ident ->
+      | IDENT "Save"; id = identref ->
 	  VernacEndProof (Proved (true,Some (id,None)))
       | IDENT "Defined" -> VernacEndProof (Proved (false,None))
-      |	IDENT "Defined"; id=base_ident -> 
+      |	IDENT "Defined"; id=identref -> 
 	  VernacEndProof (Proved (false,Some (id,None)))
       | IDENT "Suspend" -> VernacSuspend
       | IDENT "Resume" -> VernacResume None
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index cf10f0c45..e05ed48c5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -32,7 +32,8 @@ let _ =
 (* Functions overloaded by quotifier *)
 
 let induction_arg_of_constr c =
-  try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c) with _ -> ElimOnConstr c
+  try ElimOnIdent (Topconstr.constr_loc c,snd (coerce_to_id c))
+  with _ -> ElimOnConstr c
 
 let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
 
@@ -154,7 +155,7 @@ GEXTEND Gram
   bindings:
     [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding ->
           ExplicitBindings
-            ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl)
+            ((join_to_constr loc c2,NamedHyp (snd(coerce_to_id c1)), c2) :: bl)
       | n = natural; ":="; c = constr; bl = LIST0 simple_binding ->
 	  ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl)
       | c1 = constr; bl = LIST0 constr ->
@@ -292,11 +293,11 @@ GEXTEND Gram
       | IDENT "Cut"; c = constr -> TacCut c
       | IDENT "Assert"; c = constr -> TacTrueCut (None,c)
       | IDENT "Assert"; c = constr; ":"; t = constr ->
-          TacTrueCut (Some (coerce_to_id c),t)
+          TacTrueCut (Some (snd(coerce_to_id c)),t)
       | IDENT "Assert"; c = constr; ":="; b = constr ->
-          TacForward (false,Names.Name (coerce_to_id c),b)
+          TacForward (false,Names.Name (snd (coerce_to_id c)),b)
       | IDENT "Pose"; c = constr; ":="; b = constr ->
-	  TacForward (true,Names.Name (coerce_to_id c),b)
+	  TacForward (true,Names.Name (snd(coerce_to_id c)),b)
       | IDENT "Pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "Generalize"; lc = LIST1 constr -> TacGeneralize lc
       | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 24f2be581..ccac2ae73 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -96,7 +96,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
 
 (* Functions overloaded by quotifier *)
 let induction_arg_of_constr c =
-  try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c)
+  try ElimOnIdent (Topconstr.constr_loc c,snd(coerce_to_id c))
   with _ -> ElimOnConstr c
 
 let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a6d9c2420..fe8b462d8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -135,7 +135,7 @@ GEXTEND Gram
       | ":" -> false ] ]
   ;
   params:
-    [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion; c = constr
+    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; c = constr
       -> List.map (fun c -> (coe,c)) (join_binders (idl,c))
     ] ]
   ;
@@ -146,7 +146,7 @@ GEXTEND Gram
     [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ]
   ;
   ident_comma_list_tail:
-    [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
+    [ [ ","; nal = LIST1 identref SEP "," -> nal | -> [] ] ]
   ;
   decl_notation:
     [ [ "where"; ntn = STRING; ":="; c = constr; 
@@ -191,9 +191,9 @@ GEXTEND Gram
   ;
   gallina:
     (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = base_ident; ":"; c = constr ->
+    [ [ thm = thm_token; id = identref; ":"; c = constr ->
          VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ()))
-      | (f,d) = def_token; id = base_ident; b = def_body -> 
+      | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = ne_params_list -> 
 	  VernacAssumption (stre, bl)
@@ -211,7 +211,7 @@ GEXTEND Gram
     [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
   ;
   constructor:
-    [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion;
+    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion;
         c = constr -> List.map (fun id -> (coe,(id,c))) idl ] ]
   ;
   constructor_list:
@@ -224,11 +224,11 @@ GEXTEND Gram
       | ind = oneind_old_style -> [ind] ] ]
   ;
   oneind_old_style:
-    [ [ id = base_ident; ":"; c = constr; ":="; lc = constructor_list ->
+    [ [ id = identref; ":"; c = constr; ":="; lc = constructor_list ->
           (id,c,lc) ] ]
   ;
   oneind:
-    [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
+    [ [ id = identref; indpar = simple_binders_list; ":"; c = constr; 
         ":="; lc = constructor_list; ntn = OPT decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
@@ -241,7 +241,7 @@ GEXTEND Gram
       |  -> false ] ]
   ;
   onescheme:
-    [ [ id = base_ident; ":="; dep = dep; ind = global; IDENT "Sort";
+    [ [ id = identref; ":="; dep = dep; ind = global; IDENT "Sort";
         s = sort -> (id,dep,ind,s) ] ]
   ;
   schemes:
@@ -271,12 +271,12 @@ GEXTEND Gram
     [ [ l = LIST1 onecorec SEP "with" -> l ] ]
   ;
   record_field:
-    [ [ id = base_ident; oc = of_type_with_opt_coercion; t = constr ->
+    [ [ id = identref; oc = of_type_with_opt_coercion; t = constr ->
           (oc,AssumExpr (id,t))
-      | id = base_ident; oc = of_type_with_opt_coercion; t = constr;
+      | id = identref; oc = of_type_with_opt_coercion; t = constr;
 	":="; b = constr ->
 	  (oc,DefExpr (id,b,Some t))
-      | id = base_ident; ":="; b = constr ->
+      | id = identref; ":="; b = constr ->
 	  (false,DefExpr (id,b,None)) ] ]
   ;
   fields:
@@ -300,7 +300,7 @@ GEXTEND Gram
     [ [ bll = LIST1 fix_binders -> List.flatten bll ] ]
   ;
   rec_constructor:
-    [ [ c = base_ident -> Some c
+    [ [ c = identref -> Some c
       |  -> None ] ]
   ;
   gallina_ext:
@@ -308,7 +308,7 @@ GEXTEND Gram
         indl = block_old_style ->
 	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
 	  VernacInductive (f,indl')
-      | b = record_token; oc = opt_coercion; name = base_ident;
+      | b = record_token; oc = opt_coercion; name = identref;
 	ps = simple_binders_list; ":";
 	s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,c,fs)
@@ -322,7 +322,7 @@ GEXTEND Gram
       | "Fixpoint"; recs = specifrec -> VernacFixpoint recs
       | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs
       | IDENT "Scheme"; l = schemes -> VernacScheme l
-      | f = finite_token; s = csort; id = base_ident;
+      | f = finite_token; s = csort; id = identref;
 	indpar = simple_binders_list; ":="; lc = constructor_list -> 
           VernacInductive (f,[id,None,indpar,s,lc]) ] ]
   ;
@@ -332,11 +332,11 @@ GEXTEND Gram
   gallina_ext:
     [ [ 
 (* Sections *)
-	IDENT "Section"; id = base_ident -> VernacBeginSection id
-      | IDENT "Chapter"; id = base_ident -> VernacBeginSection id ] ]
+	IDENT "Section"; id = identref -> VernacBeginSection id
+      | IDENT "Chapter"; id = identref -> VernacBeginSection id ] ]
   ;
   module_vardecls:
-    [ [ id = base_ident; idl = ident_comma_list_tail; ":";
+    [ [ id = identref; idl = ident_comma_list_tail; ":";
         mty = Module.module_type -> (id::idl,mty) ] ]
   ;
   module_binders:
@@ -358,23 +358,23 @@ GEXTEND Gram
   gallina_ext:
     [ [ 
 	  (* Interactive module declaration *)
-	IDENT "Module"; id = base_ident; 
+	IDENT "Module"; id = identref; 
 	bl = module_binders_list; mty_o = OPT of_module_type; 
 	mexpr_o = OPT is_module_expr ->
 	  VernacDefineModule (id, bl, mty_o, mexpr_o)
 	  
-      | IDENT "Module"; "Type"; id = base_ident; 
+      | IDENT "Module"; "Type"; id = identref; 
 	bl = module_binders_list; mty_o = OPT is_module_type ->
 	  VernacDeclareModuleType (id, bl, mty_o)
 	  
-      | IDENT "Declare"; IDENT "Module"; id = base_ident; 
+      | IDENT "Declare"; IDENT "Module"; id = identref; 
 	bl = module_binders_list; mty_o = OPT of_module_type; 
 	mexpr_o = OPT is_module_expr ->
 	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
 
 	  (* This end a Section a Module or a Module Type *)
 
-      | IDENT "End"; id = base_ident -> VernacEndSegment id
+      | IDENT "End"; id = identref -> VernacEndSegment id
 
 
 (* Transparent and Opaque *)
@@ -387,21 +387,21 @@ GEXTEND Gram
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
 	  VernacDefinition 
-	    ((Global,CanonicalStructure),s,d,Recordobj.add_object_hook)
+	    ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
       (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
          (they were unused and undocumented) *)
 
 (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition ((Global,Coercion),s,d,Class.add_coercion_hook)
+	  VernacDefinition ((Global,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition ((Local,Coercion),s,d,Class.add_coercion_hook)
-      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
+	  VernacDefinition ((Local,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Local, f, s, t)
-      | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":";
+      | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Global, f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
@@ -417,7 +417,7 @@ GEXTEND Gram
 
 (* Implicit *)
 (*
-      | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr;
+      | IDENT "Syntactic"; "Definition"; id = identref; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   VernacSyntacticDefinition (id,c,n)
 *)
@@ -435,7 +435,7 @@ GEXTEND Gram
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
 
       | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
-	   idl = LIST1 ident SEP ","; ":"; c = constr -> VernacReserve (idl,c)
+	   idl = LIST1 identref SEP ","; ":"; c = constr -> VernacReserve (idl,c)
 
       (* For compatibility *)
       | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
@@ -486,7 +486,7 @@ GEXTEND Gram
       | IDENT "Require"; export = export_token; specif = specif_token;
         qidl = LIST1 global -> VernacRequire (Some export, specif, qidl)
 (*      | IDENT "Require"; export = export_token; specif = specif_token;
-        id = base_ident; filename = STRING -> 
+        id = identref; filename = STRING -> 
 	  VernacRequireFrom (export, specif, id, filename) *)
       | IDENT "Require"; export = export_token; specif = specif_token;
         filename = STRING -> 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8c0b6ef73..5599f5880 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -97,11 +97,11 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = base_ident; (* bl = LIST0 binder; *) ":";
+    [ [ thm = thm_token; id = identref; (* bl = LIST0 binder; *) ":";
         c = lconstr ->
           let bl = [] in
           VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
-      | (f,d) = def_token; id = base_ident; b = def_body -> 
+      | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = assum_list -> 
 	  VernacAssumption (stre, flatten_assum bl)
@@ -120,13 +120,13 @@ GEXTEND Gram
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
   ;
   gallina_ext:
-    [ [ b = record_token; oc = opt_coercion; name = base_ident;
+    [ [ b = record_token; oc = opt_coercion; name = identref;
         ps = LIST0 binder_let; ":";
-	s = lconstr; ":="; cstr = OPT base_ident; "{";
+	s = lconstr; ":="; cstr = OPT identref; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
 (* Non porté ?
-      | f = finite_token; s = csort; id = base_ident;
+      | f = finite_token; s = csort; id = identref;
         indpar = LIST0 simple_binder; ":="; lc = constructor_list -> 
           VernacInductive (f,[id,None,indpar,s,lc])
 *)
@@ -186,7 +186,7 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr; 
+    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; 
         ":="; lc = constructor_list; ntn = decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
@@ -244,7 +244,7 @@ GEXTEND Gram
   ;
   (* Inductive schemes *)
   scheme:
-    [ [ id = base_ident; ":="; dep = dep_scheme; "for"; ind = global;
+    [ [ id = identref; ":="; dep = dep_scheme; "for"; ind = global;
         IDENT "Sort"; s = sort ->
           (id,dep,ind,s) ] ]
   ;
@@ -266,12 +266,12 @@ GEXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-    [ [ id = base_ident -> (false,AssumExpr(id,CHole loc))
-      | id = base_ident; oc = of_type_with_opt_coercion; t = lconstr ->
+    [ [ id = identref -> (false,AssumExpr(id,CHole loc))
+      | id = identref; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
-      | id = base_ident; oc = of_type_with_opt_coercion;
+      | id = identref; oc = of_type_with_opt_coercion;
              t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
-      | id = base_ident; ":="; b = lconstr ->
+      | id = identref; ":="; b = lconstr ->
          match b with
              CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
            | _ -> (false,DefExpr(id,b,None)) ] ]
@@ -283,14 +283,14 @@ GEXTEND Gram
     [ [ "("; a = simple_assum_coe; ")" -> a ] ]
   ;
   simple_assum_coe:
-    [ [ idl = LIST1 base_ident; oc = of_type_with_opt_coercion; c = lconstr -> 
+    [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> 
         (oc,(idl,c)) ] ]
   ;
   constructor:
-    [ [ id = base_ident; l = LIST0 binder_let; 
+    [ [ id = identref; l = LIST0 binder_let; 
         coe = of_type_with_opt_coercion; c = lconstr ->
 	  (coe,(id,G_constrnew.mkCProdN loc l c))
-      | id = base_ident; l = LIST0 binder_let ->
+      | id = identref; l = LIST0 binder_let ->
 	  (false,(id,G_constrnew.mkCProdN loc l (CHole loc))) ] ]
   ;
   of_type_with_opt_coercion:
@@ -308,25 +308,25 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
-	IDENT "Module"; id = base_ident; 
+	IDENT "Module"; id = identref; 
 	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
 	mexpr_o = OPT is_module_expr ->
 	  VernacDefineModule (id, bl, mty_o, mexpr_o)
 	  
-      | IDENT "Module"; "Type"; id = base_ident; 
+      | IDENT "Module"; "Type"; id = identref; 
 	bl = LIST0 module_binder; mty_o = OPT is_module_type ->
 	  VernacDeclareModuleType (id, bl, mty_o)
 	  
-      | IDENT "Declare"; IDENT "Module"; id = base_ident; 
+      | IDENT "Declare"; IDENT "Module"; id = identref; 
 	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
 	mexpr_o = OPT is_module_expr ->
 	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
       (* Section beginning *)
-      | IDENT "Section"; id = base_ident -> VernacBeginSection id
-      | IDENT "Chapter"; id = base_ident -> VernacBeginSection id
+      | IDENT "Section"; id = identref -> VernacBeginSection id
+      | IDENT "Chapter"; id = identref -> VernacBeginSection id
 
       (* This end a Section a Module or a Module Type *)
-      | IDENT "End"; id = base_ident -> VernacEndSegment id
+      | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Requiring an already compiled module *)
       | IDENT "Require"; export = export_token; specif = specif_token;
@@ -361,7 +361,7 @@ GEXTEND Gram
 
   (* Module binder  *)
   module_binder:
-    [ [ "("; idl = LIST1 base_ident; ":"; mty = module_type; ")" ->
+    [ [ "("; idl = LIST1 identref; ":"; mty = module_type; ")" ->
           (idl,mty) ] ]
   ;
 
@@ -374,9 +374,9 @@ GEXTEND Gram
       ] ]
   ;
   with_declaration:
-    [ [ "Definition"; id = base_ident; ":="; c = Constr.lconstr ->
+    [ [ "Definition"; id = identref; ":="; c = Constr.lconstr ->
           CWith_Definition (id,c)
-      | IDENT "Module"; id = base_ident; ":="; qid = qualid ->
+      | IDENT "Module"; id = identref; ":="; qid = qualid ->
 	  CWith_Module (id,qid)
       ] ]
   ;
@@ -404,19 +404,19 @@ GEXTEND Gram
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
 	  VernacDefinition 
-	    ((Global,CanonicalStructure),s,d,Recordobj.add_object_hook)
+	    ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition ((Global,Coercion),s,d,Class.add_coercion_hook)
+	  VernacDefinition ((Global,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition ((Local,Coercion),s,d,Class.add_coercion_hook)
-      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
+	  VernacDefinition ((Local,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Local, f, s, t)
-      | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":";
+      | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Global, f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
@@ -433,7 +433,7 @@ GEXTEND Gram
 	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
-	   idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c)
+	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c)
 
       (* For compatibility *)
       | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->