From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 06:09:24 +0200
Subject: [lemmas] [proof] Split proof kinds into per-layer components.

We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:

- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
  pushed upwards]

We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.

More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
---
 library/decl_kinds.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'library')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 4b20016ab2..9fed8b7829 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -58,17 +58,12 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality * polymorphic * assumption_object_kind
-type definition_kind = locality * polymorphic * definition_object_kind
-
 (** Kinds used in proofs *)
 
 type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality * goal_object_kind
-
 (** Kinds used in library *)
 
 type logical_kind =
-- 
cgit v1.2.3