Consolidate reg034 into regression002
commit087a7c3f2141e49c5c98aa090659d607323ca8ae
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:37 (10 years ago)
parent7f53344
test/reg034/expecteddeleted−4
@@ -1,4 +0,0 @@
1−reg034.idr:6:5:When checking left hand side of bar:
2−Can't match on bar xs xs Refl
3−reg034.idr:9:5:When checking left hand side of foo:
4−Can't match on foo f x x Refl
test/reg034/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour --check reg034.idr
3−rm -f reg034 *.ibc
test/regression002/expected+4
@@ -47,3 +47,7 @@ reg028a.idr:17:14-19:
4747This style of tactic proof is deprecated. See %runElab for the replacement.
4848reg028a.idr:11:1:
4949tbad.qsort' is possibly not total due to: with block in tbad.qsort'
50+reg034.idr:6:5:When checking left hand side of bar:
51+Can't match on bar xs xs Refl
52+reg034.idr:9:5:When checking left hand side of foo:
53+Can't match on foo f x x Refl
test/reg034/reg034.idr → test/regression002/reg034.idrrenamed
The content is the same.
test/regression002/run+1
@@ -13,6 +13,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
1313:load reg023.idr
1414:load reg028.idr
1515:load reg028a.idr
16+:load reg034.idr
1617!
1718
1819rm -f *.ibc