better nlet rec boxing

[helm.git] / helm / software / components / library / cicElim.mli

diff --git a/helm/software/components/library/cicElim.mli b/helm/software/components/library/cicElim.mli
index f1f84c92eafcc4d575ed78fbe89889efe443d885..70c1c21678664b9fab39cc0f412bc8ead1730a0b 100644 (file)
--- 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