| Def
| Fix of int * int (* fixno, recparamno *)
| CoFix of int
- | Ind of int
+ | Ind of bool * int (* inductive, indtyno *)
| Con of int * int (* indtyno, constrno *)
-type reference = Ref of int * NUri.uri * spec
+type reference = private Ref of int * NUri.uri * spec
val eq: reference -> reference -> bool
val string_of_reference: reference -> string
+val reference_of_string: string -> reference
-
-(* CACCA *)
-val reference_of_ouri: UriManager.uri -> spec -> reference
-val ouri_of_reference: reference -> UriManager.uri
+(* given the reference of an inductive type, returns the i-th contructor *)
+val mk_constructor: int -> reference -> reference
+val mk_fix: int -> int -> reference -> reference
+val mk_cofix: int -> reference -> reference