set universe to zero in mk_subtype_of_unit

FStarLang · Jan 11, 2025 · e8a1ba2 · e8a1ba2
1 parent ff16b6e
commit e8a1ba2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/smtencoding/FStarC.SMTEncoding.Term.fst b/src/smtencoding/FStarC.SMTEncoding.Term.fst
@@ -1175,7 +1175,7 @@ let mk_Valid t        = match t.tm with
     | _ ->
         mkApp("Valid",  [t]) t.rng
 let mk_unit_type = mkApp("Prims.unit", []) norng
-let mk_subtype_of_unit v = mkApp("Prims.subtype_of", [mk_U_unknown;mk_U_unknown;v;mk_unit_type]) v.rng // GE: FIXME
+let mk_subtype_of_unit v = mkApp("Prims.subtype_of", [mk_U_zero;mk_U_zero;v;mk_unit_type]) v.rng
 let mk_HasType v t    = mkApp("HasType", [v;t]) t.rng
 let mk_HasTypeZ v t   = mkApp("HasTypeZ", [v;t]) t.rng
 let mk_IsTotFun t     = mkApp("IsTotFun", [t]) t.rng