Fix most remaining tests on branch

3 files changed, 6 insertions, 20 deletions

diff --git a/lib/flow.sail b/lib/flow.sail
index b9653828..5c182af2 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -44,18 +44,4 @@ overload operator < = {lt_int}
 overload operator >= = {gteq_int}
 overload operator > = {gt_int}
 
-$ifdef TEST
-
-val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit
-
-function __flow_test (x, y) = {
-  if lteq_atom(x, y) then {
-    _prove(constraint('n <= 'm))
-  } else {
-    _prove(constraint('n > 'm))
-  }
-}
-
-$endif
-
 $endif
diff --git a/src/specialize.ml b/src/specialize.ml
index 0f5b939c..583de600 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -54,7 +54,7 @@ open Rewriter
 open Extra_pervasives
 
 let is_typ_ord_uvar = function
-  | A_aux (A_nexp _, _) -> true
+  | A_aux (A_typ _, _) -> true
   | A_aux (A_order _, _) -> true
   | _ -> false
 
diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail
index 94b40885..86294543 100644
--- a/test/typecheck/pass/patternrefinement.sail
+++ b/test/typecheck/pass/patternrefinement.sail
@@ -3,20 +3,20 @@ default Order dec
 infix 4 ==
 
 val extz = {ocaml: "extz", lem: "extz_vec"}: forall ('n : Int) ('m : Int) ('ord : Order).
-  (atom('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
+  (int('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
 
 val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) ('a : Type).
-  vector('m, 'ord, 'a) -> atom('m)
+  vector('m, 'ord, 'a) -> int('m)
 
 val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order).
   (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool
 
-val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
-  (atom('n), atom('m)) -> bool
+val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
+  (int('n), int('m)) -> bool
 
 val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool
 
-overload operator == = {eq_vec, eq_atom, eq}
+overload operator == = {eq_vec, eq_int, eq}
 
 val test : forall 'n, 'n in {32, 64}.
   vector('n, dec, bit) -> vector(64, dec, bit)