* http://helm.cs.unibo.it/
*)
- (** 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
-* @param typeno inductive type number
-* @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 -> UriManager.uri * Cic.obj
+val init : unit -> unit