Serious bug fixed:

[helm.git] / matita / components / content_pres / content2presMatcher.ml

diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml
index 5316c92ee437eee8e6cae0f169e0506b1891ad57..8b613a524775a32bab105d8c59bc126e1d5c676a 100644 (file)
--- a/matita/components/content_pres/content2presMatcher.ml
+++ b/matita/components/content_pres/content2presMatcher.ml
@@ -67,8 +67,11 @@ struct
       | _ -> PatternMatcher.Constructor
     let tag_of_pattern = get_tag
     let tag_of_term t = get_tag t
-    let string_of_term = NotationPp.pp_term
-    let string_of_pattern = NotationPp.pp_term
+
+    (* Debugging only *)
+    (*CSC: new NCicPp.status is the best I can do now *)
+    let string_of_term = NotationPp.pp_term (new NCicPp.status)
+    let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
   end
 
   module M = PatternMatcher.Matcher (Pattern21)