package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val add_rew_rules : string -> raw_rew_rule list -> unit
val autorewrite : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> unit Proofview.tactic
val autorewrite_in : ?conds:Equality.conditions -> Names.Id.t -> unit Proofview.tactic -> string list -> unit Proofview.tactic
type rew_rule = {
  1. rew_lemma : Term.constr;
  2. rew_type : Term.types;
  3. rew_pat : Term.constr;
  4. rew_ctx : Univ.universe_context_set;
  5. rew_l2r : bool;
  6. rew_tac : Genarg.glob_generic_argument option;
}
val find_rewrites : string -> rew_rule list
val find_matches : string -> Term.constr -> rew_rule list
val auto_multi_rewrite : ?conds:Equality.conditions -> string list -> Locus.clause -> unit Proofview.tactic
val auto_multi_rewrite_with : ?conds:Equality.conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
val print_rewrite_hintdb : string -> Pp.std_ppcmds
type hypinfo = {
  1. hyp_cl : Clenv.clausenv;
  2. hyp_prf : Term.constr;
  3. hyp_ty : Term.types;
  4. hyp_car : Term.constr;
  5. hyp_rel : Term.constr;
  6. hyp_l2r : bool;
  7. hyp_left : Term.constr;
  8. hyp_right : Term.constr;
}
val find_applied_relation : ?loc:Loc.t -> bool -> Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
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