package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a t
val depth : 'a t -> int
val map_custom : ('a -> 'a) -> 'a t -> 'a t
type section_entry =
  1. | SecDefinition of Names.Constant.t
  2. | SecInductive of Names.MutInd.t
val open_section : custom:'a -> 'a t option -> 'a t
val close_section : 'a t -> 'a t option * section_entry list * Univ.ContextSet.t * 'a
val push_local : 'a t -> 'a t
val push_context : (Names.Name.t array * Univ.UContext.t) -> 'a t -> 'a t
val push_constraints : Univ.ContextSet.t -> 'a t -> 'a t
val push_constant : poly:bool -> Names.Constant.t -> 'a t -> 'a t
val push_inductive : poly:bool -> Names.MutInd.t -> 'a t -> 'a t
val all_poly_univs : 'a t -> Univ.Level.t array
type abstr_info = private {
  1. abstr_ctx : Constr.named_context;
  2. abstr_subst : Univ.Instance.t;
  3. abstr_uctx : Univ.AUContext.t;
}
val empty_segment : abstr_info
val segment_of_constant : Environ.env -> Names.Constant.t -> 'a t -> abstr_info
val segment_of_inductive : Environ.env -> Names.MutInd.t -> 'a t -> abstr_info
val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list
val is_in_section : Environ.env -> Names.GlobRef.t -> 'a t -> bool