Pltac (p.coq.8.14.0.doc.ltac2_plugin.Ltac2

Sourceval ltac2_expr : Tac2expr.raw_tacexpr Pcoq.Entry.t

Sourceval tac2expr : Tac2expr.raw_tacexpr Pcoq.Entry.t

val tac2expr_in_env : 
  (Names.Id.t CAst.t list * Tac2expr.raw_tacexpr) Pcoq.Entry.t

Sourceval q_ident : Names.Id.t CAst.t Tac2qexpr.or_anti Pcoq.Entry.t

Sourceval q_bindings : Tac2qexpr.bindings Pcoq.Entry.t

Sourceval q_with_bindings : Tac2qexpr.bindings Pcoq.Entry.t

Sourceval q_intropattern : Tac2qexpr.intro_pattern Pcoq.Entry.t

Sourceval q_intropatterns : Tac2qexpr.intro_pattern list CAst.t Pcoq.Entry.t

Sourceval q_destruction_arg : Tac2qexpr.destruction_arg Pcoq.Entry.t

Sourceval q_induction_clause : Tac2qexpr.induction_clause Pcoq.Entry.t

Sourceval q_conversion : Tac2qexpr.conversion Pcoq.Entry.t

Sourceval q_rewriting : Tac2qexpr.rewriting Pcoq.Entry.t

Sourceval q_clause : Tac2qexpr.clause Pcoq.Entry.t

Sourceval q_dispatch : Tac2qexpr.dispatch Pcoq.Entry.t

Sourceval q_occurrences : Tac2qexpr.occurrences Pcoq.Entry.t

Sourceval q_reference : Tac2qexpr.reference Tac2qexpr.or_anti Pcoq.Entry.t

Sourceval q_strategy_flag : Tac2qexpr.strategy_flag Pcoq.Entry.t

Sourceval q_constr_matching : Tac2qexpr.constr_matching Pcoq.Entry.t

Sourceval q_goal_matching : Tac2qexpr.goal_matching Pcoq.Entry.t

Sourceval q_hintdb : Tac2qexpr.hintdb Pcoq.Entry.t

Sourceval q_move_location : Tac2qexpr.move_location Pcoq.Entry.t

Sourceval q_pose : Tac2qexpr.pose Pcoq.Entry.t

Sourceval q_assert : Tac2qexpr.assertion Pcoq.Entry.t