]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content_pres/content2presMatcher.ml
Added support for hyperlinks in the goal view of the web interface.
[helm.git] / matitaB / components / content_pres / content2presMatcher.ml
index cf5d66b6a9bd9c5f3c911d83194334efc2a248af..a7b59aa52e3c3a3346f555aa1f3c3323ed53e993 100644 (file)
@@ -40,6 +40,7 @@ let get_tag term0 =
   in
   let rec aux t = 
     NotationUtil.visit_ast 
+      ~clear_interpretation:true
       ~map_xref_option:(fun _ -> None)
       ~map_case_indty:(fun _ -> None)
       ~map_case_outtype:(fun _ _ -> None)