package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 pattern_identref : Names.lident Entry.t
  • deprecated Use Prim.pattern_identref
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 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
  • deprecated Use Prim.hyp
val bar_cbrace : unit Entry.t
val strategy_level : Conv_oracle.level Entry.t