package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.library/Summary/index.html

Module `Summary`Source

This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system.

Sourcetype 'a summary_declaration = {

freeze_function : marshallable:bool -> 'a;
(*
freeze_function true is for marshalling to disk. * e.g. lazy must be forced
*)
unfreeze_function : 'a -> unit;
init_function : unit -> unit;

}

Types of global Coq states. The 'a type should be pure and marshallable by the standard OCaml marshalling function.

For tables registered during the launch of coqtop, the init_function will be run only once, during an init_summaries done at the end of coqtop initialization. For tables registered later (for instance during a plugin dynlink), init_function is used when unfreezing an earlier frozen state that doesn't contain any value for this table.

Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence the responsibility of plugins to initialize themselves properly.

Sourceval declare_summary : string -> 'a summary_declaration -> unit

Sourcemodule Dyn : Dyn.S

We provide safe projection from the summary to the types stored in it.

Sourceval declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag

All-in-one reference declaration + summary registration. It behaves just as OCaml's standard ref function, except that a declare_summary is done, with name as string. The init_function restores the reference to its initial value. The freeze_function can be overridden

Source

val ref : 
  ?freeze:(marshallable:bool -> 'a -> 'a) ->
  name:string ->
  'a ->
  'a ref

Source

val ref_tag : 
  ?freeze:(marshallable:bool -> 'a -> 'a) ->
  name:string ->
  'a ->
  'a ref * 'a Dyn.tag

Sourcemodule Local : sig ... end

Source

val declare_ml_modules_summary : 
  (string * string option) list summary_declaration ->
  unit

Special summary for ML modules. This summary entry is special because its unfreeze may load ML code and hence add summary entries. Thus is has to be recognizable, and handled properly.

For global tables registered statically before the end of coqtop launch, the following empty init_function could be used.

Sourceval nop : unit -> unit

The type frozen is a snapshot of the states of all the registered tables of the system.

Sourcetype frozen

Sourceval empty_frozen : frozen

Sourceval freeze_summaries : marshallable:bool -> frozen

Sourceval unfreeze_summaries : ?partial:bool -> frozen -> unit

Sourceval init_summaries : unit -> unit

Typed projection of the summary. Experimental API, use with CARE

Sourceval modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen

Sourceval project_from_summary : frozen -> 'a Dyn.tag -> 'a

Sourceval remove_from_summary : frozen -> 'a Dyn.tag -> frozen

Sourceval dump : unit -> (int * string) list

Debug

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Summary/index.html

Module SummarySource

Module `Summary`Source