diff options
| author | pboutill | 2010-05-05 11:53:24 +0000 |
|---|---|---|
| committer | pboutill | 2010-05-05 11:53:24 +0000 |
| commit | 9a822a9b927bb3516445779f7de99cf0ef43692e (patch) | |
| tree | 4dbe3481df76517b3884a33f091889d70638927f /kernel | |
| parent | 0583805fa794380eb9031e2c8a147fee7facacf0 (diff) | |
Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof
- ide doesn't crash anymore at any backtrack
- I don't see if vernacentries.ml did the same assumption so I didn't
change anything. (The only other use of resume_proof)
- ide still raises "NoCurrentProof" when you type a bad keyword such as
"Priint"... But at least, this on is catch somewhere !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12993 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions