]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPt.ml
added XmlAttrs attribute for specification of xml attributes directly
[helm.git] / helm / ocaml / cic_notation / cicNotationPt.ml
index 9c5257e075406dbc3b551bb2aadb10318ea18422..5ad1f0b5b1896d4006aed511b0f00761d235e337 100644 (file)
@@ -41,6 +41,8 @@ type term_attribute =
   | `IdRef of string                  (* ACic pointer *)
   | `Href of UriManager.uri list      (* hyperlinks for literals *)
   | `Level of int * Gramext.g_assoc   (* precedence, associativity *)
+  | `XmlAttrs of (string option * string * string) list
+      (* list of XML attributes: namespace, name, value *)
   ]
 
 type literal =
@@ -147,4 +149,5 @@ type phrase = (* TODO hackish: replace with TacticAst.statement or similar *)
       (* level 1 pattern, associativity, precedence, level 2 pattern *)
   | Interpretation of (string * argument_pattern list) * cic_appl_pattern
   | Render of UriManager.uri
+  | Dump  (* dump grammar *)