Merge pull request #32 from AeneasVerif/son_arrays

Add support for arrays/slices and const generics

1 files changed, 8 insertions, 0 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 0475899c..bd80769f 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -162,6 +162,14 @@ let backward_no_state_update = ref false
  *)
 let split_files = ref true
 
+(** Generate the library entry point, if the crate is split between different files.
+
+    Sometimes we want to skip this: the library entry points just includes all the
+    files in the project, and the user may want to write their own entry point, to
+    add custom includes (to include the files containing the proofs, for instance).
+ *)
+let generate_lib_entry_point = ref true
+
 (** For Lean, controls whether we generate a lakefile or not.
 
  *)