package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
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