summaryrefslogtreecommitdiff
path: root/kernel/entries.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /kernel/entries.mli
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'kernel/entries.mli')
-rw-r--r--kernel/entries.mli16
1 files changed, 11 insertions, 5 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2a77dd9..ea7c266b 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -18,8 +18,8 @@ open Term
(** {6 Local entries } *)
type local_entry =
- | LocalDef of constr
- | LocalAssum of constr
+ | LocalDefEntry of constr
+ | LocalAssumEntry of constr
(** {6 Declaration of inductive types. } *)
@@ -51,7 +51,8 @@ type mutual_inductive_entry = {
mind_entry_inds : one_inductive_entry list;
mind_entry_polymorphic : bool;
mind_entry_universes : Univ.universe_context;
- mind_entry_private : bool option }
+ mind_entry_private : bool option;
+}
(** {6 Constants (Definition/Axiom) } *)
type 'a proof_output = constr Univ.in_universe_context_set * 'a
@@ -97,14 +98,19 @@ type module_entry =
| MExpr of
module_params_entry * module_struct_entry * module_struct_entry option
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type seff_env =
+ [ `Nothing
+ (* The proof term and its universes.
+ Same as the constant_body's but not in an ephemeron *)
+ | `Opaque of Constr.t * Univ.universe_context_set ]
type side_eff =
| SEsubproof of constant * Declarations.constant_body * seff_env
| SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
type side_effect = {
- from_env : Declarations.structure_body Ephemeron.key;
+ from_env : Declarations.structure_body CEphemeron.key;
eff : side_eff;
}