From 16084065ebcff9eeba7231e687611fd9acb54887 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 23 Jul 2008 17:41:22 +0000
Subject: Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the
 opportunity to extend the class of singleton types to (possibly mutual)
 recursive types with single constructors of which all arguments are in Prop.
 This covers Acc. Acc_rect can consequently be defined in the direct way.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f70690af63..cd9e2e81f4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -598,7 +598,6 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	      poly_level = lev; 
 	    }, all_sorts
       | Inl ((issmall,isunit),ar,s) ->
-	  let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
 	  let kelim = allowed_sorts issmall isunit s in
 	    Monomorphic {
 		mind_user_arity = ar;
-- 
cgit v1.2.3