Merge pull request #187 from mtzguido/fix

Fixing config.json for new src/syntax/print directory
FStarLang · Aug 30, 2024 · 0b457c2 · 0b457c2
2 parents ceedac3 + bac7a3b
commit 0b457c2
Show file tree

Hide file tree

Showing 28 changed files with 353 additions and 347 deletions.
diff --git a/pulse2rust/src/Pulse2Rust.fst.config.json b/pulse2rust/src/Pulse2Rust.fst.config.json
@@ -19,6 +19,7 @@
     "${FSTAR_HOME}/src/reflection",
     "${FSTAR_HOME}/src/smtencoding",
     "${FSTAR_HOME}/src/syntax",
+    "${FSTAR_HOME}/src/syntax/print",
     "${FSTAR_HOME}/src/tactics",
     "${FSTAR_HOME}/src/tosyntax",
     "${FSTAR_HOME}/src/typechecker",

diff --git a/src/extraction/Extraction.fst.config.json b/src/extraction/Extraction.fst.config.json
@@ -19,6 +19,7 @@
     "${FSTAR_HOME}/src/reflection",
     "${FSTAR_HOME}/src/smtencoding",
     "${FSTAR_HOME}/src/syntax",
+    "${FSTAR_HOME}/src/syntax/print",
     "${FSTAR_HOME}/src/tactics",
     "${FSTAR_HOME}/src/tosyntax",
     "${FSTAR_HOME}/src/typechecker",

diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml
diff --git a/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml
diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml b/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml
diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Comp.ml b/src/ocaml/plugin/generated/Pulse_Checker_Comp.ml
diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml b/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml