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

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 22f896f21e12c13fa26fe2cb5d6133911385481a..3000b7311dca621bcedfc3464380621c13d3e2a6 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -86,7 +86,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let fix_sorts swap metasenv subst context meta t =
   let rec aux () = function