X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautParser.mly;h=c772837b3fbfb77554ba859a7c3d435ded38830e;hb=3e068a777bc4bda55d3c7eedc2eb8368e8acb6da;hp=9127705609c21b5ad8347817c57299a8436f7a45;hpb=9b4286fdc2d88b0d8018e5718ef055804f5cf7ac;p=helm.git

diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly
index 912770560..c772837b3 100644
--- a/helm/software/lambda-delta/automath/autParser.mly
+++ b/helm/software/lambda-delta/automath/autParser.mly
@@ -32,7 +32,7 @@
    %token TYPE PROP DEF EB E PN EXIT
     
    %start book
-   %type <Aut.book> book   
+   %type <Aut.entity list> book   
 %%
    path: MINUS {} | FS {} ;
    oftype: CN {} | CM {} ;
@@ -54,8 +54,8 @@
       | IDENT path idents { $1 :: $3 }
    ;
    qid:
-      | IDENT                    { ($1, false, []) }
-      | IDENT QT QT              { ($1, false, []) }
+      | IDENT                    { ($1, true, [])  }
+      | IDENT QT QT              { ($1, true, [])  }
       | IDENT QT local idents QT { ($1, $3, $4)    }
    ;
    term:
@@ -71,25 +71,25 @@
       | term          { [$1]     }
       | term CM terms { $1 :: $3 }
    ;
-   item:
-      | PLUS IDENT                    { A.Section (Some $2)    }
-      | PLUS TIMES IDENT              { A.Section (Some $3)    }
-      | MINUS IDENT                   { A.Section None         }
-      | EXIT                          { A.Section None         }
-      | star                          { A.Context None         }
-      | qid star                      { A.Context (Some $1)    }
-      | IDENT DEF EB sc term          { A.Block ($1, $5)       }
-      | IDENT sc term DEF EB          { A.Block ($1, $3)       }
-      | OB IDENT oftype term CB       { A.Block ($2, $4)       }
-      | IDENT DEF PN sc term          { A.Decl ($1, $5)        }
-      | IDENT sc term DEF PN          { A.Decl ($1, $3)        }
-      | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) }
-      | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) }
+   entity:
+      | PLUS IDENT                    { A.Section (Some (true, $2))  }
+      | PLUS TIMES IDENT              { A.Section (Some (false, $3)) }
+      | MINUS IDENT                   { A.Section None               }
+      | EXIT                          { A.Section None               }
+      | star                          { A.Context None               }
+      | qid star                      { A.Context (Some $1)          }
+      | IDENT DEF EB sc term          { A.Block ($1, $5)             }
+      | IDENT sc term DEF EB          { A.Block ($1, $3)             }
+      | OB IDENT oftype term CB       { A.Block ($2, $4)             }
+      | IDENT DEF PN sc term          { A.Decl ($1, $5)              }
+      | IDENT sc term DEF PN          { A.Decl ($1, $3)              }
+      | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4)       }
+      | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6)       }
    ;
-   items:
-      |            { []       }
-      | item items { $1 :: $2 }
+   entities:
+      |                 { []       }
+      | entity entities { $1 :: $2 }
    ;
    book:
-      | items eof { $1 }
+      | entities eof { $1 }
    ;