diff options
| author | Hugo Herbelin | 2020-09-27 07:35:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-14 12:23:59 +0200 |
| commit | 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b (patch) | |
| tree | 5136a7f5ef77bbc38a2a7f25c1b7684f3cd59354 /parsing | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
Deprecating wit_var to the benefit of its synonymous wit_hyp.
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_prim.mlg | 8 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 5 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 3 |
3 files changed, 9 insertions, 7 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 8069f049fd..1701830cd2 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -45,7 +45,7 @@ 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 by_notation smart_global bar_cbrace strategy_level; @@ -58,12 +58,12 @@ GRAMMAR EXTEND Gram pattern_ident: [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ] ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ 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 fa7de40a30..996aa0925c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -279,7 +279,8 @@ 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" @@ -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 fa223367f7..8e60bbf504 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -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 |