package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val write_diffs_option : string -> unit
val show_diffs : unit -> bool
val diff_goal_ide : Proof_type.goal Evd.sigma option -> Proof_type.goal -> Evd.evar_map -> Pp.t list * Pp.t
val tokenize_string : string -> string list
val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val diff_concl : ?og_s:Proof_type.goal Evd.sigma -> Evd.evar_map -> Goal.goal -> Pp.t
val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t
val log_out_ch : out_channel ref
type hyp_info = {
  1. idents : string list;
  2. rhs_pp : Pp.t;
  3. mutable done_ : bool;
}
module StringMap : sig ... end
val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list
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