diff options
| author | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
| commit | 476520ab32d3e975f6cee8aabcd04ad5fdfbbd77 (patch) | |
| tree | e8a75d0411c275635540f675449cc38b00c989fd /plugins/ltac/extraargs.mlg | |
| parent | 4bf43453ec5f635ae87a2edeb4f51d95f2d5ac67 (diff) | |
| parent | 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b (diff) | |
Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hyp
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac/extraargs.mlg')
| -rw-r--r-- | plugins/ltac/extraargs.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 863c4d37d8..ad4374dba3 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -47,7 +47,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in - register "hyp" wit_var; + register "hyp" wit_hyp; register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; @@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences GLOB_PRINTED BY { pr_occurrences } | [ ne_integer_list(l) ] -> { ArgArg l } -| [ var(id) ] -> { ArgVar id } +| [ hyp(id) ] -> { ArgVar id } END { |