diff options
| author | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
| commit | a59574c8eb4bdda60e4bdd6197e8a32574985588 (patch) | |
| tree | e15e1a0f78d23cd263726d725c93a5e6ce453465 /interp/declare.mli | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
| parent | a9f0fd89cf3bb4b728eb451572a96f8599211380 (diff) | |
Merge PR #9439: Separate variance and universe fields in inductives.
Ack-by: ppedrot
Diffstat (limited to 'interp/declare.mli')
| -rw-r--r-- | interp/declare.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index 669657af6f..6f53d6872b 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -43,7 +43,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.constant_universes_entry -> + ?univs:Entries.universes_entry -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -58,7 +58,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> Id.t -> ?types:constr -> - constr Entries.in_constant_universes_entry -> Constant.t + constr Entries.in_universes_entry -> Constant.t (** Since transparent constants' side effects are globally declared, we * need that *) |