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