Added support for hyperlinks in the goal view of the web interface.

[helm.git] / matitaB / components / content / notationPt.ml

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index 2c94ec356edb50493a46cb8f5e17cbb8b2bb8012..b624c9a8639c6e46a9ba2fef120cbdb6af3d11c8 100644 (file)
--- a/matitaB/components/content/notationPt.ml
+++ b/matitaB/components/content/notationPt.ml
@@ -51,9 +51,9 @@ type term_attribute =
   ]
 
 type literal =
-  [ `Symbol of string
-  | `Keyword of string
-  | `Number of string
+  [ `Symbol of string * (string option * string option)
+  | `Keyword of string * (string option * string option)
+  | `Number of string * (string option * string option)
   ]
 
 type case_indtype = string * href option