X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautParser.mly;h=c772837b3fbfb77554ba859a7c3d435ded38830e;hb=57a360d659425ce1ee9a69516b66a4d3c7b8eb62;hp=f974b9808397477aea0824aae3d3d5cc59a66e8e;hpb=79684e8bd0f54b5c88fff981366bd8c78dd0fbe9;p=helm.git

diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly
index f974b9808..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.unit list> book   
+   %type <Aut.entity list> book   
 %%
    path: MINUS {} | FS {} ;
    oftype: CN {} | CM {} ;
@@ -71,7 +71,7 @@
       | term          { [$1]     }
       | term CM terms { $1 :: $3 }
    ;
-   unit:
+   entity:
       | PLUS IDENT                    { A.Section (Some (true, $2))  }
       | PLUS TIMES IDENT              { A.Section (Some (false, $3)) }
       | MINUS IDENT                   { A.Section None               }
@@ -86,10 +86,10 @@
       | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4)       }
       | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6)       }
    ;
-   units:
-      |            { []       }
-      | unit units { $1 :: $2 }
+   entities:
+      |                 { []       }
+      | entity entities { $1 :: $2 }
    ;
    book:
-      | units eof { $1 }
+      | entities eof { $1 }
    ;