X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPt.ml;h=ac6a0edbd1a37a9e1684a4089b9fd8849a3e3342;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b0e9762bee7646cbd0040ec8e124c214ddb7409b;hpb=a82fc7fac28ab55650be57a127c3e3230981f72d;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index b0e9762be..ac6a0edbd 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -41,11 +41,13 @@ let fail floc msg = type href = UriManager.uri +type child_pos = [ `Left | `Right | `Inner ] + type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) - | `Href of href list (* hyperlinks for literals *) | `Level of int * Gramext.g_assoc (* precedence, associativity *) + | `ChildPos of child_pos (* position of l1 pattern variables *) | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) | `Raw of string (* unparsed version *)