the refiner was not checking that the resulting type

[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 757041451bbe7978aeb30d0dcdaf88cdf35663d8..037c5c6e2ce6b80f23e4bbacfe2f0471162e1b8b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -12,7 +12,7 @@
 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
 
 let debug s = prerr_endline (Lazy.force s);;
-(* let debug _ = ();; *)
+let debug _ = ();;
 
 module COT : Set.OrderedType 
 with type t = string * NCic.term * int * int  * NCic.term *