diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-01 09:12:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-01 09:12:05 +0000 |
| commit | 8ce32469bc02e2ecf3f1dfee56f960f19412de9b (patch) | |
| tree | 5c362d622ef2eb901ad8bdf6b6f865263294a742 | |
| parent | 0e4c44431739bd607f3eb95d6287ea35b4613e5d (diff) | |
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
| -rw-r--r-- | toplevel/discharge.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 84b46930e..bab711ea4 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, |