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 /pretyping/indrec.ml | |
| 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
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 2 |
1 files changed, 0 insertions, 2 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) |