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