package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception Parsing_error of string
type arg_source =
  1. | CmdLine
  2. | ProjectFile
type 'a sourced = {
  1. thing : 'a;
  2. source : arg_source;
}
type project = {
  1. project_file : string option;
  2. makefile : string option;
  3. install_kind : install option;
  4. use_ocamlopt : bool;
  5. native_compiler : native_compiler option;
  6. v_files : string sourced list;
  7. mli_files : string sourced list;
  8. mlg_files : string sourced list;
  9. ml_files : string sourced list;
  10. mllib_files : string sourced list;
  11. mlpack_files : string sourced list;
  12. ml_includes : path sourced list;
  13. r_includes : (path * logic_path) sourced list;
  14. q_includes : (path * logic_path) sourced list;
  15. extra_args : string sourced list;
  16. defs : (string * string) sourced list;
  17. extra_targets : extra_target sourced list;
  18. subdirs : string sourced list;
}
and extra_target = {
  1. target : string;
  2. dependencies : string;
  3. phony : bool;
  4. command : string;
}
and logic_path = string
and path = {
  1. path : string;
  2. canonical_path : string;
}
and install =
  1. | NoInstall
  2. | TraditionalInstall
  3. | UserInstall
and native_compiler =
  1. | NativeYes
  2. | NativeNo
  3. | NativeOndemand
val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> string list -> project
exception UnableToOpenProjectFile of string
val read_project_file : warning_fn:(string -> unit) -> string -> project

read_project_file warning_fn file parses file as a Coq project; use warning_fn for deprecate options; raise Parsing_error on illegal options or arguments; raise UnableToOpenProjectFile msg if the file could not be opened; fails on some illegal non-project-file options

val coqtop_args_from_project : project -> string list
val find_project_file : from:string -> projfile_name:string -> string option
val all_files : project -> string sourced list
val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list
val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list

Only uses the elements with source=CmdLine

val filter_cmdline : 'a sourced list -> 'a list

Only uses the elements with source=CmdLine

val forget_source : 'a sourced -> 'a
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct