Module Coq

module Coq: sig .. end
Interface with Coq where we define some handlers for Coq's API, and we import several definitions from Coq's standard library.

This general purpose library could be reused by other plugins.

Some salient points:




Getting Coq terms from the environment


val init_constant : string list -> string -> Term.constr

General purpose functions


type goal_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 tactic
val 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

Bindings with Coq' Standard Library


module List: sig .. end
Coq lists
module Pair: sig .. end
Coq pairs
module Bool: sig .. end
module Comparison: sig .. end
module Leibniz: sig .. end
module Option: sig .. end
module Pos: sig .. end
Coq positive numbers (pos)
module Nat: sig .. end
Coq unary numbers (peano)
module Classes: sig .. end
Coq typeclasses
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 typable

Some tacticials


val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic
time the execution of a tactic
val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic
emit debug messages to see which tactics are failing
val tclPRINT : Proof_type.tactic -> Proof_type.tactic
print the current goal

Error related mechanisms


val anomaly : string -> 'a
val user_error : string -> 'a
val warning : string -> unit

Rewriting tactics used in aac_rewrite


module Rewrite: sig .. end