diff options
Diffstat (limited to 'interp/decls.ml')
| -rw-r--r-- | interp/decls.ml | 11 |
1 files changed, 1 insertions, 10 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 = |