Do not use broken close_term_bs function.

FStarLang · Sep 12, 2024 · 44cad3e · 44cad3e
1 parent 6bdafdb
commit 44cad3e
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 57 deletions.
diff --git a/src/checker/Pulse.Extract.Main.fst b/src/checker/Pulse.Extract.Main.fst
@@ -471,8 +471,9 @@ let rec extract_dv g (p:st_term) : T.Tac ECL.term =
 and extract_dv_branch g (b:Pulse.Syntax.Base.branch) : T.Tac ECL.branch =
   let pat, body = b in
   let g, pat, bs = extract_dv_pattern g pat in
-  ECL.mk_branch pat (RT.close_term_bs (List.rev bs) // FIXME: why is the variable order reversed?!??!
-    (extract_dv g (Pulse.Checker.Match.open_st_term_bs body bs)))
+  ECL.mk_branch pat (LN.close_term_n
+    (extract_dv g (Pulse.Checker.Match.open_st_term_bs body bs))
+    (L.map fst bs))
 
 let extract_pulse_dv (g: env) (p:st_term) : T.Tac ECL.term =
   let p = erase_ghost_subterms g p in

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