From 7344d43a475559cdf4f3415dbebfd118511d5ec9 Mon Sep 17 00:00:00 2001
From: Catalin Hritcu <catalin.hritcu@gmail.com>
Date: Fri, 8 May 2015 13:55:01 +0200
Subject: [PATCH] Added #181 and #213 to the regression suite

---
 examples/bug-reports/Makefile    |  8 ++++----
 examples/bug-reports/bug181.fst  |  5 ++---
 examples/bug-reports/bug209b.fst | 10 ++++++++++
 examples/unit-tests/Makefile     |  2 +-
 4 files changed, 17 insertions(+), 8 deletions(-)
 create mode 100644 examples/bug-reports/bug209b.fst

diff --git a/examples/bug-reports/Makefile b/examples/bug-reports/Makefile
index a22e762fad6..4d68ae92749 100755
--- a/examples/bug-reports/Makefile
+++ b/examples/bug-reports/Makefile
@@ -1,10 +1,10 @@
 VERFILES=bug22.fst bug19.fst bug29.fst bug26.fst bug15.fst bug25.fst bug24.fst\
   bug28.fst bug52.fst bug23.fst bug21.fst bug96.fst bug77.fst bug92.fst bug62.fst\
   bug67.fst bug56.fst bug103.fst bug96.fst bug60.fst bug97b.fst bug101.fst\
-  bug111.fst bug116.fst bug117.fst\
-  bug122.fst bug148.fst bug161.fst bug162.fst bug170.fst bug175.fst bug178.fst\
-  bug179.fst bug186.fst bug189.fst bug190.fst bug192.fst bug195.fst\
-  bug212.fst\
+  bug111.fst bug116.fst bug117.fst bug122.fst bug124.fst \
+  bug148.fst bug161.fst bug162.fst bug170.fst bug175.fst bug178.fst\
+  bug179.fst bug181.fst bug186.fst bug189.fst bug190.fst bug192.fst bug195.fst\
+  bug212.fst bug213.fst\
   bugWildcardTelescopes.fst
 
 include ../Makefile.include
diff --git a/examples/bug-reports/bug181.fst b/examples/bug-reports/bug181.fst
index 29b4395b1db..02ca94098be 100644
--- a/examples/bug-reports/bug181.fst
+++ b/examples/bug-reports/bug181.fst
@@ -1,8 +1,7 @@
 module Bug181
 
-(* These work *)
+(* This works *)
 type t1 (t:Type) = t
-type t2 (a:Type) ('p:a->Type) = a
 
-(* This doesn't work *)
+(* This doesn't work -- now it does *)
 type t2' (a:Type) (p:a->Type) = a
diff --git a/examples/bug-reports/bug209b.fst b/examples/bug-reports/bug209b.fst
new file mode 100644
index 00000000000..b11566d868f
--- /dev/null
+++ b/examples/bug-reports/bug209b.fst
@@ -0,0 +1,10 @@
+module Bug209_EDITED
+
+val foo : #t:Type -> x:t -> Lemma (x = x)
+let foo (#t:Type) x = ()
+
+val foo2 : t:Type -> x:t -> Lemma (x = x)
+let foo2 (t:Type) x = ()
+
+val foo3 : x:'a -> Lemma (x = x)
+let foo3 'a x = ()
diff --git a/examples/unit-tests/Makefile b/examples/unit-tests/Makefile
index 68fa569753a..013874202a4 100755
--- a/examples/unit-tests/Makefile
+++ b/examples/unit-tests/Makefile
@@ -6,7 +6,7 @@ all: .all.ver testmref all-neg
 
 all-neg: $(NEGFILES)
 	-$(FSTAR) --admit_fsi Set $(STDLIB) $^
-	echo "EXPECT 33 FAILURES<------------------------------------"
+	@echo "EXPECT 33 FAILURES<------------------------------------"
 
 inverse:
 	$(FSTAR) --admit_fsi Seq $(FSTAR_HOME)/lib/classical.fst $(FSTAR_HOME)/lib/ext.fst $(FSTAR_HOME)/lib/seq.fsi inverse.fst --max_fuel 0 --max_ifuel 3 --initial_ifuel 3 --initial_fuel 0