diff options
author | 2006-06-05 23:15:51 +0000 | |
---|---|---|
committer | 2006-06-05 23:15:51 +0000 | |
commit | c9f4643f733fbfa368cb4644f95b2e233d5ad973 (patch) | |
tree | bcdad055e21901b95d8e557a9c9883e157abb66d /contrib | |
parent | b93b31918a0c583711ea9ff35ebeee18f9aba511 (diff) |
Oh le joli bug dans le kernel:
Definissons un foncteur dependant de X et Y. Alors:
Module M
: Funsig (X : T) Funsig (Y : T) Sig End
:= Functor [Y:T] Functor [X:T] Struct End
Notez les places de X et Y, a cause d'un fold_right qui aurait du etre
gauchiste. Etonnement, tout marchait tres bien en Coq, donc ce bug a
survecu discretement depuis l'ajout initial des modules. Avant que je
n'essaie d'extraire un foncteur a deux arguments...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8898 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions