diff options
| author | herbelin | 2008-07-23 17:41:22 +0000 |
|---|---|---|
| committer | herbelin | 2008-07-23 17:41:22 +0000 |
| commit | 16084065ebcff9eeba7231e687611fd9acb54887 (patch) | |
| tree | d9692bdeb1e5f6d795d90fed5e253a842ba1721f /kernel | |
| parent | ceee412ccf9dcfe85c97a1f5c6b684af04b697f2 (diff) | |
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
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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; |