aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/retroknowledge.ml19
-rw-r--r--kernel/retroknowledge.mli20
-rw-r--r--plugins/ltac/extraargs.ml439
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 ]