diff options
| author | Emilio Jesus Gallego Arias | 2019-06-25 03:10:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:36:08 +0200 |
| commit | 5f3118f6caf5f6fe2942c61ab5146bf725483937 (patch) | |
| tree | 431ceee1bc023a66e6104f777bf608c7f44e3cb0 /interp/decls.mli | |
| parent | 583c6c6204052ca177bc39d90b4aa7a645a90edc (diff) | |
[decls] Remove goal_object_kind type.
We can use logical kind for the same purpose, which is mainly
dumpglob, so `goal_object_kind` was never matched against, making this
transformation safe.
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 *) |