diff options
| author | Talia Ringer | 2019-05-22 16:09:51 -0400 |
|---|---|---|
| committer | Talia Ringer | 2019-05-22 16:09:51 -0400 |
| commit | 577db38704896c75d1db149f6b71052ef47202be (patch) | |
| tree | 946afdb361fc9baaa696df7891d0ddc03a4a8594 /kernel/declarations.ml | |
| parent | 7eefc0b1db614158ed1b322f8c6e5601e3995113 (diff) | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Merge remote-tracking branch 'origin/master' into stm+doc_hook
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 |