package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/coq-core.printing/Proof_diffs/index.html

Module Proof_diffsSource

Sourceval opt_name : string list

Name of Diffs option

Sourceval show_diffs : unit -> bool

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

Sourceval show_removed : unit -> bool

Returns true if the diffs option is "removed"

Sourceval write_color_enabled : bool -> unit

controls whether color output is enabled

Sourceval color_enabled : unit -> bool

true indicates that color output is enabled

Sourcetype diffOpt =
  1. | DiffOff
  2. | DiffOn
  3. | DiffRemoved
Sourceval string_to_diffs : string -> diffOpt
Sourceval diff_goal_ide : (Goal.goal * Evd.evar_map) 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.

Sourceval diff_goal : ?og_s:(Goal.goal * Evd.evar_map) -> 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.

Sourceval tokenize_string : string -> string list

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

Sourceval pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
Sourceval pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
Sourceval pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
Sourceval diff_concl : ?og_s:(Goal.goal * Evd.evar_map) -> Evd.evar_map -> Goal.goal -> Pp.t

Computes diffs for a single conclusion

Sourceval 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.

Sourceval log_out_ch : out_channel ref
Sourcetype hyp_info = {
  1. idents : string list;
  2. rhs_pp : Pp.t;
}
Sourceval diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list
Sourceval diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t
Sourceval notify_proof_diff_failure : string -> unit