From e431c10002ca93d1485a040e159e37be3d2b6f74 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 14 Jul 2018 10:16:48 +0100
Subject: [ltac] Remove unused functions / constructors.

Catched by compiling the ml files from ml4.
---
 plugins/ltac/extraargs.ml4 | 39 ---------------------------------------
 1 file changed, 39 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dae2582bd..dbbdbfa39 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -297,25 +297,6 @@ END
 
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
-let pr_r_nat_field natf =
-  str "nat " ++
-  match natf with
-    | Retroknowledge.NatType -> str "type"
-    | Retroknowledge.NatPlus -> str "plus"
-    | Retroknowledge.NatTimes -> str "times"
-
-let pr_r_n_field  nf =
-  str "binary N " ++
-  match nf with
-    | Retroknowledge.NPositive -> str "positive"
-    | Retroknowledge.NType -> str "type"
-    | Retroknowledge.NTwice -> str "twice"
-    | Retroknowledge.NTwicePlusOne -> str "twice plus one"
-    | Retroknowledge.NPhi -> str "phi"
-    | Retroknowledge.NPhiInv -> str "phi inv"
-    | Retroknowledge.NPlus -> str "plus"
-    | Retroknowledge.NTimes -> str "times"
-
 let pr_r_int31_field i31f =
   str "int31 " ++
   match i31f with
@@ -353,26 +334,6 @@ let pr_retroknowledge_field f =
   | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
                                            spc () ++ str "in " ++ qs group
 
-VERNAC ARGUMENT EXTEND retroknowledge_nat
-PRINTED BY pr_r_nat_field
-| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
-| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
-| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
-END
-
-
-VERNAC ARGUMENT EXTEND retroknowledge_binary_n
-PRINTED BY pr_r_n_field
-| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
-| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
-| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
-| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
-| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
-| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
-| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
-| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
-END
-
 VERNAC ARGUMENT EXTEND retroknowledge_int31
 PRINTED BY pr_r_int31_field
 | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-- 
cgit v1.2.3