Module `Pcoq.Prim`

val preident : string Entry.t
val ident : Names.Id.t Entry.t
val name : Names.lname Entry.t
val identref : Names.lident Entry.t
val univ_decl : Constrexpr.universe_decl_expr Entry.t
val ident_decl : Constrexpr.ident_decl Entry.t
val pattern_ident : Names.lident Entry.t
val pattern_identref : Names.lident Entry.t
val base_ident : Names.Id.t Entry.t
val bignat : string Entry.t
val natural : int Entry.t
val bigint : string Entry.t
val integer : int Entry.t
val string : string Entry.t
val lstring : Names.lstring Entry.t
val reference : Libnames.qualid Entry.t
val qualid : Libnames.qualid Entry.t
val fullyqualid : Names.Id.t list CAst.t Entry.t
val by_notation : (string * string option) Entry.t
val smart_global : Libnames.qualid Constrexpr.or_by_notation Entry.t
val dirpath : Names.DirPath.t Entry.t
val ne_string : string Entry.t
val ne_lstring : Names.lstring Entry.t
val hyp : Names.lident Entry.t
val var : Names.lident Entry.t
val bar_cbrace : unit Entry.t
val strategy_level : Conv_oracle.level Entry.t