Merge PR #8066: [ltac] Remove unused functions.

3 files changed, 0 insertions, 78 deletions

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index d76b05a8b..34f62defb 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -25,22 +25,6 @@ open Constr
 (* aliased type for clarity purpose*)
 type entry = Constr.t
 
-(* [field]-s are the roles the kernel can learn of. *)
-type nat_field =
-  | NatType
-  | NatPlus
-  | NatTimes
-
-type n_field =
-  | NPositive
-  | NType
-  | NTwice
-  | NTwicePlusOne
-  | NPhi
-  | NPhiInv
-  | NPlus
-  | NTimes
-
 type int31_field =
   | Int31Bits
   | Int31Type
@@ -69,9 +53,6 @@ type int31_field =
   | Int31Lxor
 
 type field =
-  (* | KEq
-     | KNat of nat_field
-     | KN of n_field *)
   | KInt31 of string*int31_field
 
 
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 281c37b85..02d961d89 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -18,21 +18,6 @@ type entry = Constr.t
 
 (** the following types correspond to the different "things"
    the kernel can learn about.*)
-type nat_field =
-  | NatType
-  | NatPlus
-  | NatTimes
-
-type n_field =
-  | NPositive
-  | NType
-  | NTwice
-  | NTwicePlusOne
-  | NPhi
-  | NPhiInv
-  | NPlus
-  | NTimes
-
 type int31_field =
   | Int31Bits
   | Int31Type
@@ -61,13 +46,8 @@ type int31_field =
   | Int31Lxor
 
 type field =
-
-(**  | KEq
-  | KNat of nat_field
-  | KN of n_field *)
   | KInt31 of string*int31_field
 
-
 (** This type represent an atomic action of the retroknowledge. It
    is stored in the compiled libraries 
    As per now, there is only the possibility of registering things
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 ]