diff options
| author | Enrico Tassi | 2019-08-02 14:08:17 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-08-02 14:08:17 +0200 |
| commit | e831ec5efd8b3b434eaf8b57b7150c3e8882e314 (patch) | |
| tree | f47a812423def7f3988da9df513d529bf327d54a /plugins/ltac | |
| parent | 12463d6d8064a79577efe0c231a768b3ef786cec (diff) | |
| parent | 845039dd1cab2066ca1ebc3cc09e726d21b1e671 (diff) | |
Merge PR #10543: Remove unused grammar nonterminals and productions
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 1e2b23bf96..21d61d1f97 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -17,7 +17,6 @@ open Genarg open Stdarg open Tacarg open Extraargs -open Pcoq.Prim open Pltac open Mod_subst open Names @@ -258,19 +257,8 @@ END open Autorewrite -let pr_orient _prc _prlc _prt = function - | true -> Pp.mt () - | false -> Pp.str " <-" - -let pr_orient_string _prc _prlc _prt (orient, s) = - pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s - } -ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY { pr_orient_string } -| [ orient(r) preident(i) ] -> { r, i } -END - TACTIC EXTEND autorewrite | [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> { auto_multi_rewrite l ( cl) } |