X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.mli;h=70c1c21678664b9fab39cc0f412bc8ead1730a0b;hb=5d0d8107649b9264ebe7d8ff2c69bf777179b0d2;hp=f1f84c92eafcc4d575ed78fbe89889efe443d885;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/library/cicElim.mli b/helm/software/components/library/cicElim.mli
index f1f84c92e..70c1c2167 100644
--- a/helm/software/components/library/cicElim.mli
+++ b/helm/software/components/library/cicElim.mli
@@ -23,19 +23,7 @@
  * 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