package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a substitutivity =
  1. | Dispose
  2. | Substitute of 'a
  3. | Keep of 'a
  4. | Anticipate of 'a
type object_name = Libnames.full_path * Names.KerName.t
type open_filter =
  1. | Unfiltered
  2. | Names of Globnames.ExtRefSet.t
type !'a object_declaration = {
  1. object_name : string;
  2. cache_function : (object_name * 'a) -> unit;
  3. load_function : int -> (object_name * 'a) -> unit;
  4. open_function : open_filter -> int -> (object_name * 'a) -> unit;
  5. classify_function : 'a -> 'a substitutivity;
  6. subst_function : (Mod_subst.substitution * 'a) -> 'a;
  7. discharge_function : (object_name * 'a) -> 'a option;
  8. rebuild_function : 'a -> 'a;
}
val simple_open : (int -> (object_name * 'a) -> unit) -> open_filter -> int -> (object_name * 'a) -> unit
val filter_and : open_filter -> open_filter -> open_filter option
val filter_or : open_filter -> open_filter -> open_filter
val in_filter_ref : Names.GlobRef.t -> open_filter -> bool
val default_object : string -> 'a object_declaration
val ident_subst_function : (Mod_subst.substitution * 'a) -> 'a
module Dyn : Dyn.S
type obj = Dyn.t
type algebraic_objects =
  1. | Objs of objects
  2. | Ref of Names.ModPath.t * Mod_subst.substitution
and t =
  1. | ModuleObject of substitutive_objects
  2. | ModuleTypeObject of substitutive_objects
  3. | IncludeObject of algebraic_objects
  4. | KeepObject of objects
  5. | ExportObject of {
    1. mpl : (open_filter * Names.ModPath.t) list;
    }
  6. | AtomicObject of obj
and objects = (Names.Id.t * t) list
and substitutive_objects = Names.MBId.t list * algebraic_objects
val declare_object_full : 'a object_declaration -> 'a Dyn.tag
val declare_object : 'a object_declaration -> 'a -> obj
val cache_object : (object_name * obj) -> unit
val load_object : int -> (object_name * obj) -> unit
val open_object : open_filter -> int -> (object_name * obj) -> unit
val subst_object : (Mod_subst.substitution * obj) -> obj
val classify_object : obj -> obj substitutivity
val discharge_object : (object_name * obj) -> obj option
val rebuild_object : obj -> obj
val local_object : string -> cache:((object_name * 'a) -> unit) -> discharge:((object_name * 'a) -> 'a option) -> 'a object_declaration
val local_object_nodischarge : string -> cache:((object_name * 'a) -> unit) -> 'a object_declaration
val global_object : string -> cache:((object_name * 'a) -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:((object_name * 'a) -> 'a option) -> 'a object_declaration
val global_object_nodischarge : string -> cache:((object_name * 'a) -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> 'a object_declaration
val superglobal_object : string -> cache:((object_name * 'a) -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:((object_name * 'a) -> 'a option) -> 'a object_declaration
val superglobal_object_nodischarge : string -> cache:((object_name * 'a) -> unit) -> subst:((Mod_subst.substitution * 'a) -> 'a) option -> 'a object_declaration
val dump : unit -> (int * string) list
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