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