X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPt.ml;h=ab484c3eb76a4db2e39d217cbe5b2731fb413c6c;hb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;hp=c702f5115703f46e8f31f35afec1ff6c0416e85b;hpb=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index c702f5115..ab484c3eb 100644
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -39,6 +39,7 @@ let loc_of_floc = function
 type term_attribute =
   [ `Loc of location                  (* source file location *)
   | `IdRef of string                  (* ACic pointer *)
+  | `Href of UriManager.uri list      (* hyperlinks for literals *)
   | `Level of int * Gramext.g_assoc   (* precedence, associativity *)
   ]
 
@@ -133,7 +134,7 @@ type argument_pattern =
   | IdentArg of int * string (* eta-depth, name *)
 
 type cic_appl_pattern =
-  | UriPattern of string
+  | UriPattern of UriManager.uri
   | VarPattern of string
   | ApplPattern of cic_appl_pattern list