package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.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 * Sorts.relevance list) -> ?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) -> pm:OblState.t -> Gentactic.glob_generic_tactic option -> Proof.t

Implementation of the Obligation n of id with tac command

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

Implementation of the Next Obligation of id with tac and Final Obligation of id with tac commands

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

Implementation of the Solve Obligations of id with tac command

Sourceval try_solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
Sourceval solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.t

Implementation of the Solve All Obligations with tac command

Sourceval show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit

Implementation of the Obligations of id command

Sourceval show_term : pm:OblState.t -> Names.Id.t option -> Pp.t

Implementation of the Preterm of id command

Sourceval admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t

Implementation of the Admit Obligations of id command

Sourceval check_program_libraries : unit -> unit
Sourceval program_inference_hook : Environ.env -> Evd.evar_map -> Evar.t -> (Evd.evar_map * EConstr.t) option