diff options
Diffstat (limited to 'src/process_file.mli')
| -rw-r--r-- | src/process_file.mli | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/src/process_file.mli b/src/process_file.mli index 97b1ba46..9f88178e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -51,25 +51,16 @@ val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs type out_type = | Lem_ast_out - | Lem_out + | Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*) val output : string -> (* The path to the library *) out_type -> (* Backend kind *) (string * Type_internal.tannot Ast.defs) list -> (*File names paired with definitions *) -(* (Types.type_defs * instances) -> (* The full environment built after all typechecking, and transforming *) - checked_module list -> (* The typechecked modules *) - Ulib.Text.t list ref -> (* alldoc accumulator *) - Ulib.Text.t list ref -> (* alldoc-inc accumulator *) - Ulib.Text.t list ref -> (* alldoc-use_inc accumulator *) *) unit -(*val output_alldoc : string -> string -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> unit*) - -(** [always_replace_files] determines whether Lem only updates modified files. +(** [always_replace_files] determines whether Sail only updates modified files. If it is set to [true], all output files are written, regardless of whether the files existed before. If it is set to [false] and an output file already exists, - the output file is only updated, if its content really changes. For some - backends like OCaml, HOL, Isabelle, this is benefitial, since it prevents them - from reprocessing these unchanged files. *) + the output file is only updated, if its content really changes. *) val always_replace_files : bool ref |