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/g_prim.mlg | |
| 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/g_prim.mlg')
| -rw-r--r-- | parsing/g_prim.mlg | 8 |
1 files changed, 4 insertions, 4 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 } ] ] ; |