diff options
| author | Pierre-Marie Pédrot | 2019-05-15 23:50:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-19 13:14:19 +0200 |
| commit | 801aed67a90ec49c15a4469e1905aa2835fabe19 (patch) | |
| tree | 9da139e5e0e5ecd8ba74806d2baa1225cee2e720 /kernel/declarations.ml | |
| parent | 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d (diff) | |
Parameterize the constant_body type by opaque subproofs.
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 649bb8725d..36ee952099 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -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, Opaqueproof.opaque) 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 |