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 : Constr.constr;
  2. rew_type : Constr.types;
  3. rew_pat : Constr.constr;
  4. rew_ctx : Univ.ContextSet.t;
  5. rew_l2r : bool;
  6. rew_tac : Genarg.glob_generic_argument option;
}
val find_rewrites : string -> rew_rule list
val find_matches : string -> Constr.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 : Environ.env -> Evd.evar_map -> string -> Pp.t
type hypinfo = {
  1. hyp_cl : Clenv.clausenv;
  2. hyp_prf : Constr.constr;
  3. hyp_ty : Constr.types;
  4. hyp_car : Constr.constr;
  5. hyp_rel : Constr.constr;
  6. hyp_l2r : bool;
  7. hyp_left : Constr.constr;
  8. hyp_right : Constr.constr;
}
val find_applied_relation : ?loc:Loc.t -> bool -> Environ.env -> Evd.evar_map -> Constr.constr -> bool -> hypinfo