Tidbit

FStarLang · Nov 29, 2023 · 2d9db05 · 2d9db05
1 parent 4ad7019
commit 2d9db05
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/lib/Checker.ml b/lib/Checker.ml
@@ -688,7 +688,7 @@ and infer' env e =
       check env TBool e1;
       let t = infer env e2 in
       if t = TUnit || t = TAny then
-        t (* loops that end in return can be typed with TAny *)
+        TAny (* loops that end in return can be typed with TAny *)
       else
         checker_error env "%a, while loop is neither tany or tunit" ploc env.location
 

diff --git a/lib/Simplify.ml b/lib/Simplify.ml
@@ -1066,7 +1066,7 @@ and hoist_expr loc pos e =
       (* We now allow IfThenElse nodes directly under IfThenElse, on the basis
        * that the outer IfThenElse is properly positioned under a let-binding.
        * let_if_to_assign will know how to deal with this. *)
-      if pos = UnderStmtLet || pos = UnderConditional then
+      if pos = UnderStmtLet || pos = UnderConditional || Options.rust () then
         lhs1, mk (EIfThenElse (e1, e2, e3))
       else
         let b, body, cont = mk_named_binding "ite" t (EIfThenElse (e1, e2, e3)) in