Merge pull request #134 from AeneasVerif/protz_relax

Relax failing assertion
AeneasVerif · Jan 11, 2025 · aff3b63 · aff3b63
2 parents 0cc48e6 + 3d16334
commit aff3b63
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml
@@ -730,7 +730,8 @@ let smallest =
   end
 
 let rec find_terminal_incr i e =
-  assert (e.typ = TUnit);
+  if e.typ <> TUnit && e.typ <> TAny then
+    Krml.Warn.failwith "e_then has type: %a\n" ptyp e.typ;
   let ( let* ) = Option.bind in
   let hoist e = Krml.DeBruijn.subst_n e (List.init i (fun _ -> Krml.Helpers.eunit)) in
   match e.node with