package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val tac2expr_in_env : (Names.Id.t CAst.t list * Tac2expr.raw_tacexpr) Pcoq.Entry.t

Quoted entries. To be used for complex notations.

val q_with_bindings : Tac2qexpr.bindings Pcoq.Entry.t
val q_intropatterns : Tac2qexpr.intro_pattern list CAst.t Pcoq.Entry.t
val q_destruction_arg : Tac2qexpr.destruction_arg Pcoq.Entry.t
val q_induction_clause : Tac2qexpr.induction_clause Pcoq.Entry.t
val q_constr_matching : Tac2qexpr.constr_matching Pcoq.Entry.t