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:

we use Caml's module system to mimic Coq's one, and avoid cluttering the namespace;
we also provide several handlers for standard coq tactics, in order to provide a unified setting (we replace functions that modify the evar_map by functions that operate on the whole goal, and repack the modified evar_map with it).

Getting Coq terms from the environment

val init_constant_constr : string list -> string -> Constr.t

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

General purpose functions

type goal_sigma = Proof_type.goal Evd.sigma

val resolve_one_typeclass : Proof_type.goal Evd.sigma -> EConstr.types -> EConstr.constr * goal_sigma

val cps_resolve_one_typeclass : ?error:Pp.t ->
       EConstr.types -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic

val nf_evar : goal_sigma -> EConstr.constr -> EConstr.constr

val evar_unit : goal_sigma -> EConstr.constr -> EConstr.constr * goal_sigma

val evar_binary : goal_sigma -> EConstr.constr -> EConstr.constr * goal_sigma

val evar_relation : goal_sigma -> EConstr.constr -> EConstr.constr * goal_sigma

val cps_evar_relation : EConstr.constr -> (EConstr.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 ->
       EConstr.constr -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic

val retype : EConstr.constr -> Proof_type.tactic

val decomp_term : Evd.evar_map ->
       EConstr.constr ->
       (EConstr.constr, EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t)
       Constr.kind_of_term

val lapp : EConstr.constr lazy_t -> EConstr.constr array -> EConstr.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:EConstr.rel_context ->
       goal_sigma ->
       EConstr.constr -> (EConstr.constr * EConstr.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 : Pp.t -> 'a

val warning : string -> unit

Rewriting tactics used in aac_rewrite

module Rewrite: sig .. end