module Coq:sig
..end
This general purpose library could be reused by other plugins.
Some salient points:
val init_constant : string list -> string -> Term.constr
typegoal_sigma =
Proof_type.goal Tacmach.sigma
val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma
val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma
val cps_resolve_one_typeclass : ?error:string ->
Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val nf_evar : goal_sigma -> Term.constr -> Term.constr
val fresh_evar : goal_sigma -> Term.types -> Term.constr * goal_sigma
val evar_unit : goal_sigma -> Term.constr -> Term.constr * goal_sigma
val evar_binary : goal_sigma -> Term.constr -> Term.constr * goal_sigma
val evar_relation : goal_sigma -> Term.constr -> Term.constr * goal_sigma
val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
cps_mk_letin name v
binds the constr v
using a letin tacticval cps_mk_letin : string ->
Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val decomp_term : Term.constr -> (Term.constr, Term.types) Term.kind_of_term
val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr
module List:sig
..end
module Pair:sig
..end
module Bool:sig
..end
module Comparison:sig
..end
module Leibniz:sig
..end
module Option:sig
..end
module Pos:sig
..end
module Nat:sig
..end
module Classes:sig
..end
module Relation:sig
..end
module Transitive:sig
..end
module Equivalence:sig
..end
val match_as_equation : ?context:Term.rel_context ->
goal_sigma ->
Term.constr -> (Term.constr * Term.constr * Relation.t) option
match_as_equation ?context goal c
try to decompose c as a
relation applied to two terms. An optionnal rel_context can be
provided to ensure that the term remains typableval tclTIME : string -> Proof_type.tactic -> Proof_type.tactic
val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic
val tclPRINT : Proof_type.tactic -> Proof_type.tactic
val anomaly : string -> 'a
val user_error : string -> 'a
val warning : string -> unit
module Rewrite:sig
..end