Consolidate reg056 into regression002
commite2f1da2a5c0bcf30e5c93cb54c8c257703842fd1
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:52 (10 years ago)
parent2bf2038
test/reg056/expecteddeleted−2
@@ -1,2 +0,0 @@
1−reg056.idr:7:7:dodgy n m Refl is a valid case
2−reg056.idr:10:6:nonk Refl is a valid case
test/reg056/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg056.idr -o reg056
3−rm -f *.ibc
test/regression002/expected+2
@@ -107,3 +107,5 @@ When checking an application of constructor Foo.CAny:
107107 Attempting concrete match on polymorphic argument: Nothing
108108reg055a.idr:13:7:When checking left hand side of Foo.apply:
109109Can't match on apply (\x => \y => x) a
110+reg056.idr:7:7:dodgy n m Refl is a valid case
111+reg056.idr:10:6:nonk Refl is a valid case
test/reg056/reg056.idr → test/regression002/reg056.idrrenamed
The content is the same.
test/regression002/run+1
@@ -25,6 +25,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
2525:load reg054.idr
2626:load reg055.idr
2727:load reg055a.idr
28+:load reg056.idr
2829!
2930
3031rm -f *.ibc