diff options
Diffstat (limited to 'interp/decls.mli')
| -rw-r--r-- | interp/decls.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/interp/decls.mli b/interp/decls.mli index ce29197891..05e4be0de6 100644 --- a/interp/decls.mli +++ b/interp/decls.mli @@ -45,11 +45,6 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context Logical | Hypothesis | Axiom *) -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind (** Kinds used in library *) @@ -59,9 +54,6 @@ type logical_kind = | IsDefinition of definition_object_kind | IsProof of theorem_kind -(** Operations *) -val logical_kind_of_goal_kind : goal_object_kind -> logical_kind - (** This module manages non-kernel informations about declarations. It is either non-logical informations or logical informations that have no place to be (yet) in the kernel *) |