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).

type tactic = unit Proofview.tactic

type lazy_ref = Names.GlobRef.t Stdlib.Lazy.t

Getting Coq terms from the environment

val get_fresh : lazy_ref -> Constr.constr

val get_efresh : lazy_ref -> EConstr.constr

val find_global : string -> lazy_ref

General purpose functions

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

val evar_binary : Environ.env ->
       Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr

val evar_relation : Environ.env ->
       Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr

val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic

val tclRETYPE : EConstr.constr -> unit Proofview.tactic

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

Bindings with Coq' Standard Library

module List: sig .. end

Coq lists

module Pair: sig .. end

Coq pairs

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 Equivalence: sig .. end

val match_as_equation : ?context:EConstr.rel_context ->
       Environ.env ->
       Evd.evar_map ->
       EConstr.constr -> (EConstr.constr * EConstr.constr * Relation.t) option

match_as_equation ?context env sigma c try to decompose c as a relation applied to two terms.

Some tacticials

val tclTIME : string -> tactic -> tactic

time the execution of a tactic

val tclDEBUG : string -> unit Proofview.tactic

emit debug messages to see which tactics are failing

val tclPRINT : unit Proofview.tactic

print the current goal

Error related mechanisms

val anomaly : string -> 'a

val user_error : Pp.t -> 'a

val warning : string -> unit

Helpers

val show_proof : Declare.Proof.t -> unit

print the current proof term

Rewriting tactics used in aac_rewrite

module Rewrite: sig .. end