diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/decls.ml | 11 | ||||
| -rw-r--r-- | interp/decls.mli | 8 |
2 files changed, 1 insertions, 18 deletions
diff --git a/interp/decls.ml b/interp/decls.ml index 52685e0666..b802dbe9c3 100644 --- a/interp/decls.ml +++ b/interp/decls.ml @@ -48,13 +48,8 @@ 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 *) +(** Kinds *) type logical_kind = | IsPrimitive @@ -62,10 +57,6 @@ type logical_kind = | IsDefinition of definition_object_kind | IsProof of theorem_kind -let logical_kind_of_goal_kind = function - | DefinitionBody d -> IsDefinition d - | Proof s -> IsProof s - (** Data associated to section variables and local definitions *) type variable_data = 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 *) |