From c13a3b61c9b1a714c50bcf0ec371a4effe1ff627 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Jun 2019 15:09:40 +0200
Subject: Attach the universe polymorphic status to sections.

The previous implementation allowed to dynamically decide whether a section
would be monomorphic or polymorphic at the first definition of a variable
or a constraint. Instead of relying on this delayed decision, we set the
universe polymorphic property directly at the time of the section definition.
---
 library/lib.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
index 01366ddfd0..fe6bf69ec4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,7 +147,7 @@ val library_part :  GlobRef.t -> DirPath.t
 
 (** {6 Sections } *)
 
-val open_section : Id.t -> unit
+val open_section : poly:bool -> Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
-- 
cgit v1.2.3