exception Can_t_eliminate
(** internal error while generating elimination principle *)
-exception Elim_failure of string
+exception Elim_failure of string Lazy.t
(** @param sort target sort, defaults to Type
* @param uri inductive type uri
* @raise Failure
* @raise Can_t_eliminate
* @return Cic constant corresponding to the required elimination principle
+* and its uri
*)
-val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.obj
-
+val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj