X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=19f9e359e85aff4844fc66a3f00812f0e864acf7;hb=0663e736012a6bf2af56758181252289e79352d2;hp=9373e54b43a1de051f743a2581220677abaf4df8;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 9373e54b4..19f9e359e 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -160,8 +160,8 @@ EXTEND
 	let to_spec id = GrafiteAst.Ident id in
 	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "discriminate"; t = tactic_term ->
-        GrafiteAst.Discriminate (loc, t)
+    | IDENT "destruct"; t = tactic_term ->
+        GrafiteAst.Destruct (loc, t)
     | IDENT "elim"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
 	GrafiteAst.Elim (loc, what, using, num, idents)
@@ -191,8 +191,6 @@ EXTEND
     | IDENT "goal"; n = int ->
         GrafiteAst.Goal (loc, n)
     | IDENT "id" -> GrafiteAst.IdTac loc
-    | IDENT "injection"; t = tactic_term ->
-        GrafiteAst.Injection (loc, t)
     | IDENT "intro"; ident = OPT IDENT ->
         let idents = match ident with None -> [] | Some id -> [id] in
         GrafiteAst.Intros (loc, Some 1, idents)
@@ -575,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 ->