aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.ml
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-10 18:34:49 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-10 18:34:49 +0000
commit7b80c5023071a0dead641da1d14078489f6e6f4c (patch)
treeb51d714d85937ba2281244dea1d913bcef055b3c /ide/minilib.ml
parent2856df4134047a06df13f5cff3d8c62158c03779 (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/minilib.ml')
0 files changed, 0 insertions, 0 deletions