diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-09 18:42:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-09 18:42:56 +0000 |
| commit | ed54c8c767c6a3dfe9ce453c57bd849c20df7951 (patch) | |
| tree | e815574b1a97a990a2e2ac9327a09bc6257becd3 /proofs/redexpr.ml | |
| parent | 7caefa690b0a9c61a85798a050a7f9f62972ab7d (diff) | |
Suppresion de la catégorie des inductifs singletons larges dont
l'élimination vers Set était autorisée: comme souligné par Benjamin,
c'est incompatible avec EM + AC (report rev 9633 8.1)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/redexpr.ml')
0 files changed, 0 insertions, 0 deletions