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)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index abd49ee4b7..88bb055dcc 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) 
-- 
cgit v1.2.3