package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coq-core.stm/Vcs/Make/index.html

Module Vcs.MakeSource

Parameters

module K : Kind

Signature

Sourcemodule Branch : sig ... end
Sourcetype id = OT.t
Sourcetype 'a kind_gen = 'a K.t
Sourcetype branch_info = {
  1. kind : kind;
  2. root : id;
  3. pos : id;
}
Sourcetype ('diff, 'info, 'property_data) t
Sourceval empty : id -> ('diff, 'info, 'property_data) t
Sourceval current_branch : ('e, 'i, 'c) t -> Branch.t
Sourceval branches : ('e, 'i, 'c) t -> Branch.t list
Sourceval get_branch : ('e, 'i, 'c) t -> Branch.t -> branch_info
Sourceval reset_branch : ('e, 'i, 'c) t -> Branch.t -> id -> ('e, 'i, 'c) t
Sourceval branch : ('e, 'i, 'c) t -> ?root:id -> ?pos:id -> Branch.t -> kind -> ('e, 'i, 'c) t
Sourceval delete_branch : ('e, 'i, 'c) t -> Branch.t -> ('e, 'i, 'c) t
Sourceval merge : ('diff, 'i, 'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> Branch.t -> ('diff, 'i, 'c) t
Sourceval commit : ('diff, 'i, 'c) t -> id -> 'diff -> ('diff, 'i, 'c) t
Sourceval rewrite_merge : ('diff, 'i, 'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> Branch.t -> ('diff, 'i, 'c) t
Sourceval checkout : ('e, 'i, 'c) t -> Branch.t -> ('e, 'i, 'c) t
Sourceval set_info : ('e, 'info, 'c) t -> id -> 'info -> ('e, 'info, 'c) t
Sourceval get_info : ('e, 'info, 'c) t -> id -> 'info option
Sourcemodule Dag : Dag.S with type node = id with type node = OT.t with type NodeSet.t = Set.Make(OT).t with type NodeSet.elt = OT.t
Sourceval dag : ('diff, 'info, 'cdata) t -> ('diff, 'info, 'cdata) Dag.t
Sourceval create_property : ('e, 'i, 'c) t -> id list -> 'c -> ('e, 'i, 'c) t
Sourceval property_of : ('e, 'i, 'c) t -> id -> 'c Dag.Property.t list
Sourceval delete_property : ('e, 'i, 'c) t -> 'c Dag.Property.t -> ('e, 'i, 'c) t
Sourceval gc : ('e, 'info, 'c) t -> ('e, 'info, 'c) t * Dag.NodeSet.t
Sourceval reachable : ('e, 'info, 'c) t -> id -> Dag.NodeSet.t
OCaml

Innovation. Community. Security.