Fix test

First few were failing due to `is_inj` not being found. Use codes
for all of them.

tests/bug-reports/BugBoxInjectivity.fst

@@ -1,5 +1,8 @@
 module BugBoxInjectivity
 
+open FStar.Functions
+module CC = FStar.Cardinality.Universes
+
 //The original bug; using an indirection to subvert the injectivity check
 let mytype1 = Type u#1
 
@@ -10,7 +13,7 @@ let inj_my_t (#a:Type u#1) (x:my_t a)
 : Lemma (x == My #a)
 = ()
 
-[@@expect_failure]
+[@@expect_failure [19]]
 let my_t_injective : squash (is_inj my_t) = 
   introduce forall f0 f1.
       my_t f0 == my_t f1 ==> f0 == f1
@@ -28,7 +31,7 @@ let inj_t (#a:Type u#1) (x:t a)
 : Lemma (x == Mk #a)
 = ()
 
-[@@expect_failure]
+[@@expect_failure [19]]
 let t_injective : squash (is_inj t) = 
   introduce forall f0 f1.
       t f0 == t f1 ==> f0 == f1
@@ -38,8 +41,6 @@ let t_injective : squash (is_inj t) =
     inj_t #f1 (coerce_eq () (Mk #f0)) 
   )
 
-open FStar.Functions
-module CC = FStar.Cardinality.Universes
 //Disabling the injectivity check on parameters is inconsistent
 #push-options "--ext 'compat:injectivity'"
 noeq
@@ -73,7 +74,7 @@ type ceq (#a:Type) x : a -> Type =
 let test a (x y:a) (h:ceq #a x y) : Lemma (x == y) = ()
 
 //But without collapsing
-[@expect_failure]
+[@expect_failure [19]]
 let bad (h0:ceq true true) (h1:ceq false false) : Lemma (true == false) =
   let Refl = h0 in
   let Refl = h1 in
@@ -89,22 +90,22 @@ noeq
 type test3 (a:idx) : Type u#1 =
   | Mk3 : test3 a
 
-[@@expect_failure]
+[@@expect_failure [19]]
 let eq_test3_should_fail (x0 : test3 A1) (x1 : test3 A2) : unit =
   assert (test3 A1 == test3 A2)
 
 let case0 (x0 : test3 A1) (x1 : test3 A2) : Lemma False =
  assume (test3 A1 == test3 A2);
  assume (~ (Mk3 #A1 == coerce_eq () (Mk3 #A2)))
 
-[@@expect_failure]
+[@@expect_failure [228]]
 let case1 (x0 : test3 A1) (x1 : test3 A2) : Lemma False =
  assume (test3 A1 == test3 A2);
  assert (~ (Mk3 #A1 == coerce_eq () (Mk3 #A2)))
     by (T.norm [delta;primops];
         T.trefl ())
 
-[@@expect_failure]
+[@@expect_failure [228]]
 let case2 (x0 : test3 A1) (x1 : test3 A2) : Lemma False =
  assume (test3 A1 == test3 A2);
  assert (~ (Mk3 #A1 == coerce_eq () (Mk3 #A2)))
@@ -122,7 +123,7 @@ let case5 (x0 : test3 A1) (x1 : test3 A2) : Lemma (test3 A1 == test3 A2 ==> Mk3
  assume (test3 A1 == test3 A2);
  assert (Mk3 #A1 == coerce_eq () (Mk3 #A2))
     by (T.norm [delta;primops;nbe];
-        T.trivial()) //this can be proven by the normalizer alone; nor by nbe
+        T.trivial()) //this can be proven by the normalizer alone; and by nbe
 
 let case6 (x0 : test3 A1) (x1 : test3 A2) : Lemma (test3 A1 == test3 A2 ==> Mk3 #A1 == coerce_eq () (Mk3 #A2)) =
  assume (test3 A1 == test3 A2);