diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 18:18:21 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 18:18:21 +0100 |
| commit | f4818831f8661cab43ec0261d78140b0693d1381 (patch) | |
| tree | 36293713b05c08778e4e47b970053002b7811687 /test-suite/output/Tactics.out | |
| parent | e480926a93acca46e1e4ce25213dd4340a3b1266 (diff) | |
Fix test-suite after change in "context" printing.
Diffstat (limited to 'test-suite/output/Tactics.out')
| -rw-r--r-- | test-suite/output/Tactics.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 9949658c4..239edd1da 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -1,4 +1,4 @@ Ltac f H := split; [ a H | e H ] Ltac g := match goal with - | |- context [if ?X then _ else _] => case X + | |- context [ if ?X then _ else _ ] => case X end |