From 29db87956fb866fd63ce47b90ae2412d71ffc02d Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 12 Dec 2006 18:44:29 +0000 Subject: Correction du bug #1273, deuxième version (avec des shémas d'elimination plus simples) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/indrec.ml | 2 -- toplevel/command.ml | 15 +++++++++++---- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index abd49ee4b..88bb055dc 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -425,8 +425,6 @@ let mis_make_indrec env sigma listdepkind mib = if (mis_is_recursive_subset (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) - (* mis_is_recursive_subset do not care about mutually recursive calls so: *) - || (nparams-nparrec > 0) then let env' = push_rel_context lnamesparrec env in it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) diff --git a/toplevel/command.ml b/toplevel/command.ml index aee4afb43..ff5b3bd3b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -216,12 +216,19 @@ let declare_one_elimination ind = let env = Global.env () in let sigma = Evd.empty in let elim_scheme = Indrec.build_indrec env sigma ind in - let npars = mib.mind_nparams_rec in + let npars = + (* if a constructor of [ind] contains a recursive call, the scheme + is generalized only wrt recursively uniform parameters *) + if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) + then + mib.mind_nparams_rec + else + mib.mind_nparams in let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in let kelim = elim_sorts (mib,mip) in - (* in case the inductive has a type elimination, generates only one - induction scheme, the other ones share the same code with the - apropriate type *) + (* in case the inductive has a type elimination, generates only one + induction scheme, the other ones share the same code with the + apropriate type *) if List.mem InType kelim then let elim = make_elim (new_sort_in_family InType) in let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in -- cgit v1.2.3