diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-10 18:34:49 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-10 18:34:49 +0000 |
commit | 7b80c5023071a0dead641da1d14078489f6e6f4c (patch) | |
tree | b51d714d85937ba2281244dea1d913bcef055b3c /ide/preferences.mli | |
parent | 2856df4134047a06df13f5cff3d8c62158c03779 (diff) |
Revert "Check if recursive calls are guarded before printing "Proof completed"."
because guard condition is checked at Qed anyway and it can be expensivise to
check it twice. Use explicitly "Guarded" if you want this information.
But the wrong proof completed is now the right no more subgoals ...
Of course, we would like an incrementally checked guard condition one
day !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14177 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.mli')
0 files changed, 0 insertions, 0 deletions