From dcdb59e6f51b11f9804ea0a9cd9566303df2c2b9 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 13:31:56 +0200
Subject: follows G. Gilbert's suggestion to have polymorphism following a flag

---
 tuto1/src/simple_declare.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index c05907ad4f..5fd0b2e84b 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -17,7 +17,8 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
 let packed_declare_definition ident value_with_constraints =
   let body, ctx = value_with_constraints in
   let sigma = Evd.from_ctx ctx in
-  let k = (Decl_kinds.Global, true, Decl_kinds.Definition) in
+  let k = (Decl_kinds.Global,
+           Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
   let udecl = Univdecls.default_univ_decl in
   let nohook = Lemmas.mk_hook (fun _ x -> x) in
   ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
-- 
cgit v1.2.3