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.ml | |
| 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.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 = |