package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.vernac/Declare/Obls/index.html

Module Declare.OblsSource

Sourcetype fixpoint_kind =
  1. | IsFixpoint of Names.lident option list
  2. | IsCoFixpoint
Sourceval check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit

Check obligations are properly solved before closing the what_for section / module

Sourceval default_tactic : unit Proofview.tactic ref
Sourcetype progress =
  1. | Remain of int
    (*

    n obligations remaining

    *)
  2. | Dependent
    (*

    Dependent on other definitions

    *)
  3. | Defined of Names.GlobRef.t
    (*

    Defined as id

    *)

Resolution status of a program

Prepare API, to be removed once we provide the corresponding 1-step API

Sourceval add_definition : pm:OblState.t -> info:Info.t -> cinfo:Constr.types CInfo.t -> opaque:bool -> uctx:UState.t -> ?body:Constr.t -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?using:Vernacexpr.section_subset_expr -> ?obl_hook:OblState.t Hook.g -> RetrieveObl.obligation_info -> OblState.t * progress

Start a Program Definition c proof. uctx udecl impargs kind scope poly etc... come from the interpretation of the vernacular; `obligation_info` was generated by RetrieveObl It will return whether all the obligations were solved; if so, it will also register c with the kernel.

Sourceval add_mutual_definitions : pm:OblState.t -> info:Info.t -> cinfo:Constr.types CInfo.t list -> opaque:bool -> uctx:UState.t -> bodies:Constr.t list -> possible_guard:Pretyping.possible_guard -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?using:Vernacexpr.section_subset_expr -> ?obl_hook:OblState.t Hook.g -> RetrieveObl.obligation_info list -> OblState.t

Start a Program Fixpoint declaration, similar to the above, except it takes a list now.

Sourceval obligation : (int * Names.Id.t option * Constrexpr.constr_expr option) -> pm:OblState.t -> Genarg.glob_generic_argument option -> Proof.t

Implementation of the Obligation command

Sourceval next_obligation : pm:OblState.t -> ?final:bool -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t

Implementation of the Next Obligation and Final Obligation commands

Sourceval solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t * progress

Implementation of the Solve Obligation command

Sourceval solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.t
Sourceval try_solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
Sourceval show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit
Sourceval show_term : pm:OblState.t -> Names.Id.t option -> Pp.t
Sourceval admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t
Sourceval check_program_libraries : unit -> unit