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 /doc/RecTutorial/RecTutorial.tex | |
| 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 'doc/RecTutorial/RecTutorial.tex')
0 files changed, 0 insertions, 0 deletions