diff options
| author | Gaëtan Gilbert | 2019-09-27 17:26:26 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-02 14:38:48 +0200 |
| commit | 994edaf989c0232b5c7de70a2f8ccb46c557da95 (patch) | |
| tree | 46f5633c8e3e351a232836f951b8946f71dcf256 /kernel/section.mli | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
Loosen restrictions on mixing universe mono/polymorphism in sections
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
Diffstat (limited to 'kernel/section.mli')
| -rw-r--r-- | kernel/section.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/section.mli b/kernel/section.mli index c1026a2980..fc3ac141e4 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -21,16 +21,13 @@ val empty : 'a t val is_empty : 'a t -> bool (** Checks whether there is no opened section *) -val is_polymorphic : 'a t -> bool -(** Checks whether last opened section is polymorphic *) - (** {6 Manipulating sections} *) type section_entry = | SecDefinition of Constant.t | SecInductive of MutInd.t -val open_section : poly:bool -> custom:'a -> 'a t -> 'a t +val open_section : custom:'a -> 'a t -> 'a t (** Open a new section with the provided universe polymorphic status. Sections can be nested, with the proviso that polymorphic sections cannot appear inside a monomorphic one. A custom data can be attached to this section, |