diff options
| author | Gaëtan Gilbert | 2019-05-21 12:41:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-21 12:41:57 +0200 |
| commit | afb1a427debbc32aef1b2df0b31aa9cf8938b687 (patch) | |
| tree | acaa552dfc9a6f72bf90303f1d437b8856a9112a /kernel/declarations.ml | |
| parent | 897088fb8f4769bacca9fc289387096283835cd6 (diff) | |
| parent | e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c (diff) | |
Merge PR #10174: Further cleanup of the side-effect machinery
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5551742c02..36ee952099 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -47,10 +47,10 @@ type inline = int option transparent body, or an opaque one *) (* Global declarations (i.e. constants) can be either: *) -type 'a constant_def = +type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) - | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) + | OpaqueDef of 'opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) type universes = @@ -87,9 +87,9 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) -type constant_body = { +type 'opaque constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) - const_body : Constr.t Mod_subst.substituted constant_def; + const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def; const_type : types; const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; @@ -246,7 +246,7 @@ type module_alg_expr = (** A component of a module structure *) type structure_field_body = - | SFBconst of constant_body + | SFBconst of Opaqueproof.opaque constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body | SFBmodtype of module_type_body |