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 !'a object_declaration = {
  1. object_name : string;
  2. cache_function : (Libnames.object_name * 'a) -> unit;
  3. load_function : int -> (Libnames.object_name * 'a) -> unit;
  4. open_function : int -> (Libnames.object_name * 'a) -> unit;
  5. classify_function : 'a -> 'a substitutivity;
  6. subst_function : (Mod_subst.substitution * 'a) -> 'a;
  7. discharge_function : (Libnames.object_name * 'a) -> 'a option;
  8. rebuild_function : 'a -> 'a;
}
val default_object : string -> 'a object_declaration
val ident_subst_function : (Mod_subst.substitution * 'a) -> 'a
type obj
val declare_object_full : 'a object_declaration -> ('a -> obj) * (obj -> 'a)
val declare_object : 'a object_declaration -> 'a -> obj
val object_tag : obj -> string
val cache_object : (Libnames.object_name * obj) -> unit
val load_object : int -> (Libnames.object_name * obj) -> unit
val open_object : int -> (Libnames.object_name * obj) -> unit
val subst_object : (Mod_subst.substitution * obj) -> obj
val classify_object : obj -> obj substitutivity
val discharge_object : (Libnames.object_name * obj) -> obj option
val rebuild_object : obj -> obj
val dump : unit -> (int * string) list