package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val opt_name : string list
val show_diffs : unit -> bool
val show_removed : unit -> bool
val write_color_enabled : bool -> unit
val color_enabled : unit -> bool
type diffOpt =
  1. | DiffOff
  2. | DiffOn
  3. | DiffRemoved
val string_to_diffs : string -> diffOpt
val diff_goal_ide : Goal.goal Evd.sigma option -> Goal.goal -> Evd.evar_map -> Pp.t list * Pp.t
val diff_goal : ?og_s:Goal.goal Evd.sigma -> Goal.goal -> Evd.evar_map -> Pp.t
val tokenize_string : string -> string list
val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val diff_concl : ?og_s:Goal.goal Evd.sigma -> Evd.evar_map -> Goal.goal -> Pp.t
val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t
val log_out_ch : Stdlib.out_channel Stdlib.ref
type hyp_info = {
  1. idents : string list;
  2. rhs_pp : Pp.t;
  3. mutable done_ : bool;
}
val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list
val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t
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