diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2003-01-30 20:08:19 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2003-01-30 20:08:19 +0000 |
| commit | 05a120275c557e95c73c7c2bdd1e2725197d3bd0 (patch) | |
| tree | bf821d1442a08211cc7abbcb059f6ab5d579d15a /REGISTER | |
| parent | d4b3bb61d84cb2cd831a43b65dc55ef25fa8abaa (diff) | |
Bug correction in the find-and-forget function for coq: in Coq v74, no
prompt is return if an empty command is send ("\n"), so if the command
is empty, we send proof-no-command (if not, backtracking state
preserving command stays indefinitely in "proof process busy" state).
Diffstat (limited to 'REGISTER')
0 files changed, 0 insertions, 0 deletions