]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/text/txtParser.mly
"Not" is no longer a definition
[helm.git] / helm / software / lambda-delta / text / txtParser.mly
index 05af001e74fe8fd2a56f149f873062c74a427830..6aafbb5517f01b1ec909f8b081995e75cd100edd 100644 (file)
@@ -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
       | TH   { T.Th  }
    ;
    xentity:
-      | REQUIRE ids
-         { Some (T.Require $2)                           }
       | GRAPH ID
          { Some (T.Graph $2)                             }
       | decl comment ID CN term
          { 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                             
          { None                                          }
    ;
    start: 
-      | GRAPH {} | decl {} | def {} 
-      | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+      | GRAPH {} | decl {} | def {} | GEN {} |
+      | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
    ;
    entry:
       | xentity       { $1, false }