diff options
| author | Enrico Tassi | 2019-07-26 14:30:04 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-07-26 20:25:24 +0200 |
| commit | c2e78d0731bda2bab5525eaaf1659213eec8c4fd (patch) | |
| tree | 7d52fbefe8d276c7b13003fff81f64e451b5b6a1 /pgshell | |
| parent | 6361916d4d80828fd0bcc92c575c59e831b3fa8f (diff) | |
Backtrack -> BackTo
href: coq/coq#10574
* Define a variable coq--retract-naborts to handle the communication
of [coq-find-and-forget -> coq-empty-action-list-command] that used
to be done through the third argument of Backtrack.
* Refactor coq-empty-action-list-command, replacing the occurrences of
string-match with string-match-p.
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions