New tactic clear; new syntax # _; to introduce and immediately clear an

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

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index f79b458419a9728421c21e814adf4054eade5cf0..8c5dcae76d0d700e5a93156faa32bdb5eae66ba0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -27,7 +27,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg