package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type fixpoint_kind =
  1. | IsFixpoint of Names.lident option list
  2. | IsCoFixpoint
val check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit

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

val default_tactic : unit Proofview.tactic ref
type 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

val prepare_obligation : name:Names.Id.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info

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

val add_definition : pm:OblState.t -> cinfo:Constr.types CInfo.t -> info:Info.t -> ?obl_hook:OblState.t Hook.g -> ?term:Constr.t -> uctx:UState.t -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?opaque:bool -> 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.

val add_mutual_definitions : (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list -> pm:OblState.t -> info:Info.t -> ?obl_hook:OblState.t Hook.g -> uctx:UState.t -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?opaque:bool -> ntns:Metasyntax.notation_interpretation_decl list -> fixpoint_kind -> OblState.t

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

val 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

val 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

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

Implementation of the Solve Obligation command

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct