diff options
| author | Jim Fehrle | 2019-07-21 09:37:02 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-07-26 16:09:24 -0700 |
| commit | 845039dd1cab2066ca1ebc3cc09e726d21b1e671 (patch) | |
| tree | d131f4836f25458908d98a75f4c435df7fe2e2df /plugins/ltac | |
| parent | 00abd9ed2ac31d0655fa1f07a919b9739c8ec5fb (diff) | |
Remove unused grammar productions
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) } |