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

0 files changed, 0 insertions, 0 deletions