package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val locate_global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.t
val global_of_extended_global : Globnames.extended_global_reference -> Names.GlobRef.t
val global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.t
val global_constant_with_alias : Libnames.qualid -> Names.Constant.t
val global_inductive_with_alias : Libnames.qualid -> Names.inductive
val global_constructor_with_alias : Libnames.qualid -> Names.constructor
val smart_global : ?head:bool -> Libnames.qualid Constrexpr.or_by_notation -> Names.GlobRef.t