diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-10 14:57:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-10 14:57:51 +0000 |
| commit | d4e696cb8145701356fb9993a8a97e970e83ff8c (patch) | |
| tree | f0d5a97a0f42824beff6b306b8f4e8ffaf3dee6b /TODO | |
| parent | c702789588f6673a847312e5dab8ea998c80597b (diff) | |
Backtrack sur l'"optimisation" de admit (révision 11084). Comme le
fait remarquer Bruno, c'est ne pas anodin de laisser croire qu'on
admet une conjecture alors qu'on admet uniquement la conclusion de
cette conjecture, conclusion qui peut être incohérente et qui ne le
serait pas si on avait gardé le contexte du but.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11089 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'TODO')
0 files changed, 0 insertions, 0 deletions