package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.vernac/VernacControl/index.html

Module `VernacControl`Source

Sourcetype 'state control_entry

Partially interpreted control flags.

Sourcetype 'state control_entries = 'state control_entry list

Sourceval from_syntax : Vernacexpr.control_flag list -> unit control_entries

Translate from syntax and add default timeout.

Sourcetype ('st0, 'st) with_local_state = {

with_local_state : 'a. 'st0 -> (unit -> 'a) -> 'st * 'a;

}

with_local_state state0 f should run f with state0 installed, capture the state produced by running f and revert the global state afterwards.

Sourceval trivial_state : (unit, unit) with_local_state

Source

val under_control : 
  loc:Loc.t option ->
  with_local_state:('state0, 'state) with_local_state ->
  'state0 control_entries ->
  noop:'b ->
  (unit -> 'b) ->
  'state control_entries * 'b

under_control ~loc ~with_local_state control ~noop f runs f () in the context given by the control.

If the control cause execution to end with no more work to be done and no error (eg Fail when f raised an exception) then noop is returned.

Sourceval after_last_phase : loc:Loc.t option -> _ control_entries -> bool

Print any final messages (eg from Time) and raise final exceptions (eg from Fail when the command did not fail). The returned boolean tells if we should be noop (Fail where the command failed or Succeed where it succeeded).