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 : out_channel 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