From 845039dd1cab2066ca1ebc3cc09e726d21b1e671 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 21 Jul 2019 09:37:02 -0700
Subject: Remove unused grammar productions

---
 plugins/ltac/extratactics.mlg | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'plugins/ltac')

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) }
-- 
cgit v1.2.3