- we simplified the parser return values

[helm.git] / helm / software / lambda-delta / automath / autParser.mly

diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly
index ed5da5a647a7c8ccf64a0555d09d2e707b0da658..e90ba3b7c12b963702c22f47e9e7805dcd9c605b 100644 (file)
--- a/helm/software/lambda-delta/automath/autParser.mly
+++ b/helm/software/lambda-delta/automath/autParser.mly
@@ -24,11 +24,10 @@
  */
 
 %{
+   module O = Options
    module A = Aut
 
-   let debug = false
-
-   let _ = Parsing.set_trace debug
+   let _ = Parsing.set_trace !O.debug_parser
 %}
    %token <int> NUM
    %token <string> IDENT
@@ -36,7 +35,7 @@
    %token TYPE PROP DEF EB E PN EXIT
     
    %start entry
-   %type <Aut.command option * bool> entry   
+   %type <Aut.command option> entry   
 %%
    path: MINUS {} | FS {} ;
    oftype: CN {} | CM {} ;
@@ -81,22 +80,21 @@
       | star {} | IDENT {} | OB {} 
    ; 
    entity:
-      | PLUS IDENT                    { Some (A.Section (Some (true, $2)))  }
-      | PLUS TIMES IDENT              { Some (A.Section (Some (false, $3))) }
-      | MINUS IDENT                   { Some (A.Section None)               }
-      | EXIT                          { Some (A.Section None)               }
-      | star                          { Some (A.Context None)               }
-      | qid star                      { Some (A.Context (Some $1))          }
-      | IDENT DEF EB sc term          { Some (A.Block ($1, $5))             }
-      | IDENT sc term DEF EB          { Some (A.Block ($1, $3))             }
-      | OB IDENT oftype term CB       { Some (A.Block ($2, $4))             }
-      | IDENT DEF PN sc term          { Some (A.Decl ($1, $5))              }
-      | IDENT sc term DEF PN          { Some (A.Decl ($1, $3))              }
-      | IDENT DEF expand term sc term { Some (A.Def ($1, $6, $3, $4))       }
-      | IDENT sc term DEF expand term { Some (A.Def ($1, $3, $5, $6))       }
-      | eof                           { None                                }
+      | 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)       }
    ;
    entry:
-      | entity       { $1, false }
-      | entity start { $1, true }
-   
+      | entity start { Some $1 }
+      | eof          { None    }
+   ;