diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 17:26:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 17:26:30 +0200 |
| commit | cd9a2e9e59d87801790859ddd26d225d71be7f7c (patch) | |
| tree | 905ed87fc20331c441c3a6620ec7c3624c7b4b8e /test-suite/output | |
| parent | bf39345125d66d3efd9f934be91200013f57841c (diff) | |
Fixing test-suite
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/ltac.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 9a60afe5f..7e2610c7d 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -12,6 +12,6 @@ Goal True. assert (H:= eq_refl ((fun x => x) 1)). let HT := type of H in lazymatch goal with -| H1 : HT |- _ => idtac "matched" +| H1 : HT |- _ => idtac end. Abort. |