CPrimitivestype t = val parse : string -> tCan raise Not_found. Beware that this is not exactly the reverse of to_string below.
type args_red = arg_kind listval hash : t -> intval to_string : t -> stringval arity : t -> intIncluding parameters
val nparams : t -> intSpecial Entries for Register *
type 'a prim_type = | PT_int63 : unit prim_type |
| PT_float64 : unit prim_type |
| PT_array : (UVars.Instance.t * ind_or_type) prim_type |
and 'a prim_ind = | PIT_bool : unit prim_ind |
| PIT_carry : ind_or_type prim_ind |
| PIT_pair : (ind_or_type * ind_or_type) prim_ind |
| PIT_cmp : unit prim_ind |
| PIT_f_cmp : unit prim_ind |
| PIT_f_class : unit prim_ind |
and ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type |
| PITT_type : 'a prim_type * 'a -> ind_or_type |
| PITT_param : int -> ind_or_type |
val typ_univs : 'a prim_type -> UVars.AbstractContext.tval prim_type_of_string : string -> prim_type_exCan raise Not_found
val prim_type_to_string : 'a prim_type -> stringval op_or_type_univs : op_or_type -> UVars.AbstractContext.tval prim_ind_to_string : 'a prim_ind -> stringval op_or_type_of_string : string -> op_or_typeCan raise Not_found
val op_or_type_to_string : op_or_type -> stringval parse_op_or_type : ?loc:Loc.t -> string -> op_or_typeval univs : t -> UVars.AbstractContext.tval types : t -> Constr.rel_context * ind_or_type list * ind_or_typeParameters * Reduction relevant arguments * output type
XXX we could reify universes in ind_or_type (currently polymorphic types like array are assumed to use universe 0).