From f480f07c232b4bcc4ea67bf0577e267d0fdc35f4 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 12 May 2015 17:22:09 +0200
Subject: Fix my previous commit on ~polyprop

 Oups, sorry, I should have compiled the stdlib in full. Not only
 the ~polyprop wasn't propagated properly, but Matthieu made it be
 false by default somewhere instead of true. Argl...
---
 kernel/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 088b99b9e0..4c1614bac1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -213,7 +213,7 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
-let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
+let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
   type_of_inductive_gen ~polyprop env mip args
 
 (* The max of an array of universes *)
-- 
cgit v1.2.3