From 8ce32469bc02e2ecf3f1dfee56f960f19412de9b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Oct 2011 09:12:05 +0000
Subject: Fixing critical part of bug #2504. Not all inductive types in Type
 are polymorphic and only for inductive polymorphic types is the conclusion of
 the arity irrelevant. Refreshing at discharge time (that indtypes.ml expects
 for retyping) should be done only for polymorphic types. For monomorphic
 inductive types in Type, the type level is possibly related to universe
 constraints stored in the section and it must not be changed. [Alternatively,
 discharge should not retype inductive types from scratch, but instead
 generalize them over the section variables, the same way it does for
 definitions/axioms. But that's another story.]

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14501 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/discharge.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 84b46930e6..bab711ea42 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -65,13 +65,20 @@ let abstract_inductive hyps nparams inds =
     inds'
   in (params',ind'')
 
+let refresh_polymorphic_type_of_inductive (_,mip) =
+  match mip.mind_arity with
+  | Monomorphic s ->
+      s.mind_user_arity
+  | Polymorphic ar ->
+      let ctx = List.rev mip.mind_arity_ctxt in
+      mkArity (List.rev ctx,Termops.new_Type_sort())
 
 let process_inductive sechyps modlist mib =
   let nparams = mib.mind_nparams in
   let inds =
     array_map_to_list
       (fun mip ->
-	 let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in
+	 let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in
 	 let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
 	 (mip.mind_typename,
 	  arity,
-- 
cgit v1.2.3