]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPt.ml
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationPt.ml
index c702f5115703f46e8f31f35afec1ff6c0416e85b..ab484c3eb76a4db2e39d217cbe5b2731fb413c6c 100644 (file)
@@ -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