Added #181 and #213 to the regression suite

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

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

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 = ()

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