Merge remote-tracking branch 'origin/main' into nik_binary_search

FStarLang · Sep 6, 2024 · e7b2906 · e7b2906
2 parents 2fb5240 + 1aa9274
commit e7b2906
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/checker/Pulse.Typing.fst b/src/checker/Pulse.Typing.fst
@@ -71,7 +71,7 @@ let mk_sq_eq2 (u:universe)
               (e0 e1:term) 
   : term
   = let eq = mk_eq2 u t e0 e1 in
-    (tm_pureapp (tm_uinst (as_fv R.squash_qn) [u]) None eq)
+    (tm_pureapp (tm_uinst (as_fv R.squash_qn) [u_zero]) None eq)
 
 let mk_slprop_eq (e0 e1:term) : term =
   mk_eq2 u2 tm_slprop e0 e1

diff --git a/src/ocaml/plugin/generated/Pulse_Typing.ml b/src/ocaml/plugin/generated/Pulse_Typing.ml