package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/ltac_plugin/Ltac_plugin/G_obligations/index.html

Module Ltac_plugin.G_obligationsSource

Sourceval set_default_tactic : Vernacexpr.locality_flag -> Tacexpr.glob_tactic_expr -> unit
Sourceval get_default_tactic : unit -> Vernacexpr.locality_flag * unit Proofview.tactic
Sourceval print_default_tactic : unit -> Pp.t
Sourceval with_tac : (Genarg.glob_generic_argument option -> 'a) -> Tacexpr.raw_tactic_expr option -> 'a
Sourcemodule Tactic = Pltac
Sourcetype 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
Sourceval obligation : pm:Declare.OblState.t -> (int * Names.Id.t option * Constrexpr.constr_expr option) -> Tacexpr.raw_tactic_expr option -> Declare.Proof.t
Sourceval next_obligation : pm:Declare.OblState.t -> Names.Id.t option -> Tacexpr.raw_tactic_expr option -> Declare.Proof.t