package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val opt_name : string list

Name of Diffs option

val show_diffs : unit -> bool

Returns true if the diffs option is "on" or "removed"

val show_removed : unit -> bool

Returns true if the diffs option is "removed"

val write_color_enabled : bool -> unit

controls whether color output is enabled

val color_enabled : unit -> bool

true indicates that color output is enabled

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

Computes the diff between the goals of two Proofs and returns the highlighted lists of hypotheses and conclusions.

If the strings used to display the goal are not lexable (this is believed unlikely), this routine will generate a Diff_Failure. This routine may also raise Diff_Failure under some "impossible" conditions.

If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff.

val diff_goal : ?og_s:Goal.goal Evd.sigma -> Goal.goal -> Evd.evar_map -> Pp.t

Computes the diff between two goals

If the strings used to display the goal are not lexable (this is believed unlikely), this routine will generate a Diff_Failure. This routine may also raise Diff_Failure under some "impossible" conditions.

If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff.

val tokenize_string : string -> string list

Convert a string to a list of token strings using the lexer

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

Computes diffs for a single conclusion

val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t

Generates a map from np to op that maps changed goals to their prior forms. The map doesn't include entries for unchanged goals; unchanged goals will have the same goal id in both versions.

op and np must be from the same proof document and op must be for a state before np.

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
val notify_proof_diff_failure : string -> unit
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