package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a delayed_universes =
  1. | PrivateMonomorphic of 'a
  2. | PrivatePolymorphic of int * Univ.ContextSet.t
type opaquetab
type opaque
val empty_opaquetab : opaquetab
type cooking_info = {
  1. modlist : work_list;
  2. abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t;
}
type opaque_proofterm = (Constr.t * unit delayed_universes) option
type indirect_accessor = {
  1. access_proof : Names.DirPath.t -> int -> opaque_proofterm;
  2. access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> Constr.t * unit delayed_universes;
}
val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
val subst_opaque : Mod_subst.substitution -> opaque -> opaque
val discharge_opaque : cooking_info -> opaque -> opaque
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : ?except:Future.UUIDSet.t -> opaquetab -> opaque_proofterm array * int Future.UUIDMap.t