]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicElim.mli
Every exception that used to have type string is now a string Lazy.t.
[helm.git] / helm / ocaml / cic_proof_checking / cicElim.mli
index 0d81b7a60b9198d8f4374431e58a7581231623d4..a00ebff423c98276e37fefb24a133edb86597284 100644 (file)
@@ -28,7 +28,7 @@
 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