diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-12 18:44:29 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-12 18:44:29 +0000 |
| commit | 29db87956fb866fd63ce47b90ae2412d71ffc02d (patch) | |
| tree | fe449d7deca91b7f77a0404b59996c7fa3a11c71 | |
| parent | 0e416b95c593bf315885f83e17575fcd26470c0f (diff) | |
Correction du bug #1273, deuxième version (avec des shémas d'elimination plus simples)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rw-r--r-- | 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 |