package coq-core

  1. Overview
  2. Docs
package coq-core
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 meta_file =
  1. | Absent
  2. | Present of string
  3. | Generate of string
type 'a project = {
  1. project_file : string option;
  2. makefile : string option;
  3. native_compiler : native_compiler option;
  4. docroot : string option;
  5. files : string sourced list;
  6. cmd_line_files : string sourced list;
  7. meta_file : meta_file;
  8. ml_includes : path sourced list;
  9. r_includes : (path * logic_path) sourced list;
  10. q_includes : (path * logic_path) sourced list;
  11. extra_args : string sourced list;
  12. defs : (string * string) sourced list;
  13. extra_data : 'a;
}
and logic_path = string
and path = {
  1. path : string;
  2. canonical_path : string;
}
and native_compiler =
  1. | NativeYes
  2. | NativeNo
  3. | NativeOndemand
val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> parse_extra:(string -> string list -> 'a -> (string list * 'a) option) -> 'a -> string list -> 'a project
exception UnableToOpenProjectFile of string
val read_project_file : warning_fn:(string -> unit) -> string -> unit 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 files_by_suffix : string sourced list -> string list -> 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 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 Blog 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