diff options
| author | bertot | 2006-11-05 18:03:52 +0000 |
|---|---|---|
| committer | bertot | 2006-11-05 18:03:52 +0000 |
| commit | 7d0a4d8c93d47a076f58a9ec6ad0cbba100c79a1 (patch) | |
| tree | c2ec7abfce56f3fcfc1398f02f26754a2533a884 /kernel/type_errors.ml | |
| parent | af0e34649ea94994fcdbf9b39ae78af21842a794 (diff) | |
fixes PR#1269 about function: there is no reason well founded induction is
limited to only Set and not any type in Type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9340 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions