X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=19f9e359e85aff4844fc66a3f00812f0e864acf7;hb=e53c9d7cf1a5d3d33c41cad5b046b018a62a9d2d;hp=ab15311dfd219c09bb7af3cc51b920724b62f071;hpb=070e79b6e7ec986dd5fcdee24857956f6a4a9221;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index ab15311df..19f9e359e 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -573,6 +573,15 @@ EXTEND
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
+    | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
+      refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
+                   refl = tactic_term -> refl ] ;
+      sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
+                   sym = tactic_term -> sym ] ;
+      trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
+                   trans = tactic_term -> trans ] ;
+      "as" ; id = IDENT ->
+       GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
   ]];
   lexicon_command: [ [
       IDENT "alias" ; spec = alias_spec ->