diff options
| author | David Aspinall | 2009-09-04 08:39:56 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-04 08:39:56 +0000 |
| commit | a3397a0cdd8af9f9cde954b3647a45476df91439 (patch) | |
| tree | e1fd96ca46c45da16b2c2b6877911eea37cae620 /coq | |
| parent | 2caea10ae59fa63882ed60cb92a6d4250832e0ba (diff) | |
Remove proof-no-command
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -498,7 +498,7 @@ If locked span already has a state number, thne do nothing. Also updates (int-to-string span-staten) (int-to-string proofdepth) naborts))) - (if (string-equal ans "") proof-no-command ; not here because if + (if (string-equal ans "") nil ; [was proof-no-command]not here because if ;; we backtrack a state preserving command, we must do ;; *nothing*, not even a CR (in > v74, no prompt is returned ;; with "\n") @@ -592,8 +592,8 @@ If locked span already has a state number, thne do nothing. Also updates (if (> nundos 0) (concat "Undo " (int-to-string nundos) ". ")))) - (if (null ans) proof-no-command;; FIXME: this is an error really (assert nil); - (if (string-equal ans "") proof-no-command ; not here because if + (if (null ans) nil;; [was proof-no-command] FIXME: this is an error really (assert nil); + (if (string-equal ans "") nil ;; [was proof-no-command] ; not here because if ; we backtrack a state preserving command, we must do ; *nothing*, not even a CR (in v74, no prompt is returned ; with "\n") |