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 pattern_ident : 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 fields : (Names.Id.t list * Names.Id.t) Entry.t
val fullyqualid : Names.Id.t list CAst.t Entry.t
val by_notation : (string * string option) Entry.t
val dirpath : Names.DirPath.t Entry.t
val ne_string : string Entry.t
val ne_lstring : Names.lstring Entry.t
val bar_cbrace : unit Entry.t
val strategy_level : Conv_oracle.level Entry.t