diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 10 | ||||
| -rw-r--r-- | parsing/g_prim.mlg | 15 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 7 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 7 |
4 files changed, 19 insertions, 20 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 1ec83c496a..644493a010 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram | "10" LEFTA [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) } | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } - | "@"; lid = pattern_identref; args = LIST1 identref -> + | "@"; lid = pattern_ident; args = LIST1 identref -> { let { CAst.loc = locid; v = id } = lid in let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ] @@ -252,7 +252,7 @@ GRAMMAR EXTEND Gram | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; appl_arg: - [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } + [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) } | c=operconstr LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: @@ -261,12 +261,12 @@ GRAMMAR EXTEND Gram | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } - | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } - | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } + | "?"; "["; id = identref; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id.CAst.v, None) } + | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id.CAst.v, None) } | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] ; inst: - [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ] + [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ] ; evar_instance: [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 270662b824..1701830cd2 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -45,9 +45,9 @@ let test_minus_nat = GRAMMAR EXTEND Gram GLOBAL: - bignat bigint natural integer identref name ident var preident + bignat bigint natural integer identref name ident hyp preident fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation + ne_string string lstring pattern_ident by_notation smart_global bar_cbrace strategy_level; preident: [ [ s = IDENT -> { s } ] ] @@ -56,17 +56,14 @@ GRAMMAR EXTEND Gram [ [ s = IDENT -> { Id.of_string s } ] ] ; pattern_ident: - [ [ LEFTQMARK; id = ident -> { id } ] ] - ; - pattern_identref: - [ [ id = pattern_ident -> { CAst.make ~loc id } ] ] - ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> { CAst.make ~loc id } ] ] + [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ] ; identref: [ [ id = ident -> { CAst.make ~loc id } ] ] ; + hyp: (* as identref, but interpreted as an hypothesis in tactic notations *) + [ [ id = identref -> { id } ] ] + ; field: [ [ s = FIELD -> { Id.of_string s } ] ] ; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 723f08413e..996aa0925c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -279,14 +279,15 @@ module Prim = let strategy_level = Entry.create "strategy_level" (* parsed like ident but interpreted as a term *) - let var = Entry.create "var" + let hyp = Entry.create "hyp" + let var = hyp let name = Entry.create "name" let identref = Entry.create "identref" let univ_decl = Entry.create "univ_decl" let ident_decl = Entry.create "ident_decl" let pattern_ident = Entry.create "pattern_ident" - let pattern_identref = Entry.create "pattern_identref" + let pattern_identref = pattern_ident (* To remove in 8.14 *) (* A synonym of ident - maybe ident will be located one day *) let base_ident = Entry.create "base_ident" @@ -504,7 +505,7 @@ let () = Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); Grammar.register0 wit_ident (Prim.ident); - Grammar.register0 wit_var (Prim.var); + Grammar.register0 wit_hyp (Prim.hyp); Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ae9a7423c2..8e60bbf504 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -156,8 +156,8 @@ module Prim : val identref : lident Entry.t val univ_decl : universe_decl_expr Entry.t val ident_decl : ident_decl Entry.t - val pattern_ident : Id.t Entry.t - val pattern_identref : lident Entry.t + val pattern_ident : lident Entry.t + val pattern_identref : lident Entry.t [@@ocaml.deprecated "Use Prim.pattern_identref"] val base_ident : Id.t Entry.t val bignat : string Entry.t val natural : int Entry.t @@ -173,7 +173,8 @@ module Prim : val dirpath : DirPath.t Entry.t val ne_string : string Entry.t val ne_lstring : lstring Entry.t - val var : lident Entry.t + val hyp : lident Entry.t + val var : lident Entry.t [@@ocaml.deprecated "Use Prim.hyp"] val bar_cbrace : unit Entry.t val strategy_level : Conv_oracle.level Entry.t end |