X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtParser.mly;h=6aafbb5517f01b1ec909f8b081995e75cd100edd;hb=4efe53bc2098939c255d5b03941212549f89a1bd;hp=05af001e74fe8fd2a56f149f873062c74a427830;hpb=4c157ac5c58f34fffc98289c2d2e71032d584a83;p=helm.git

diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly
index 05af001e7..6aafbb551 100644
--- a/helm/software/lambda-delta/text/txtParser.mly
+++ b/helm/software/lambda-delta/text/txtParser.mly
@@ -33,7 +33,7 @@
    %token <int> IX
    %token <string> ID STR
    %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO 
-   %token REQUIRE GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF
+   %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option * bool> entry
@@ -123,8 +123,6 @@
       | TH   { T.Th  }
    ;
    xentity:
-      | REQUIRE ids
-         { Some (T.Require $2)                           }
       | GRAPH ID
          { Some (T.Graph $2)                             }
       | decl comment ID CN term
@@ -133,6 +131,12 @@
          { Some (T.Entity ($1, $3, $2, $5))              }
       | def comment ID EQ term CN term
          { Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+      | GEN term
+         { Some (T.Generate [$2])                        }
+      | GEN terms
+         { Some (T.Generate $2)                          }      
+      | REQ ids
+         { Some (T.Require $2)                           }
       | OPEN ID                           
          { Some (T.Section (Some $2))                    }
       | CLOSE                             
@@ -143,8 +147,8 @@
          { None                                          }
    ;
    start: 
-      | GRAPH {} | decl {} | def {} 
-      | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+      | GRAPH {} | decl {} | def {} | GEN {} |
+      | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
    ;
    entry:
       | xentity       { $1, false }