]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_refiner/nCicRefineUtil.ml
Most warnings turned into errors and avoided
[helm.git] / matita / components / ng_refiner / nCicRefineUtil.ml
index 30ae05577e59eacb35c63daf95b0316afb67c7ba..508e891f3e2b59932dd8c5c2de00ae7b29438b84 100644 (file)
@@ -25,8 +25,8 @@
 
 (* $Id: cicUtil.ml 10153 2009-07-28 15:17:51Z sacerdot $ *)
 
-exception Meta_not_found of int
-exception Subst_not_found of int
+(*exception Meta_not_found of int
+exception Subst_not_found of int*)
 
 (* syntactic_equality up to the                 *)
 (* distinction between fake dependent products  *)