+ (** can't build the required elimination principle (e.g. elimination from Prop
+ * to Set *)
+exception Can_t_eliminate
+
+ (** internal error while generating elimination principle *)
+exception Elim_failure of string Lazy.t
+
+(** @param sort target sort
+* @param uri inductive type uri