From b96e45b1714c12daa1127e8bf14467eea07ebe17 Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 2 Jan 2004 20:28:44 +0000 Subject: meilleure presentation des commentaires du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/ast.ml | 2 +- parsing/ast.mli | 2 +- parsing/g_basevernac.ml4 | 69 ++++++++++++++++++++++++++---------------------- parsing/g_ltac.ml4 | 2 +- parsing/g_module.ml4 | 4 +-- parsing/g_proofs.ml4 | 6 ++--- parsing/g_proofsnew.ml4 | 6 ++--- parsing/g_tactic.ml4 | 11 ++++---- parsing/g_tacticnew.ml4 | 2 +- parsing/g_vernac.ml4 | 58 ++++++++++++++++++++-------------------- parsing/g_vernacnew.ml4 | 58 ++++++++++++++++++++-------------------- 11 files changed, 113 insertions(+), 107 deletions(-) (limited to 'parsing') 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" -> -- cgit v1.2.3