]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.ml
removed debug prerr_endline
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml
index bfc535a3c35f59b204ccd8d7706d7df3fb15d8af..9f5fd193e9d170c05ef4fe9473e175c9805d251d 100644 (file)
@@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec"
 let macro = Grammar.Entry.create grammar "macro"
 let script = Grammar.Entry.create grammar "script"
 let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
 
@@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body =
     vars body
 
 EXTEND
-  GLOBAL: term term0 statement;
+  GLOBAL: term term0 statement statements;
   int: [
     [ num = NUM ->
         try
@@ -586,6 +587,10 @@ EXTEND
     | com = comment -> TacticAst.Comment (loc, com)
     ]
   ];
+  statements: [
+    [ l = LIST0 [ statement ] -> l 
+    ]  
+  ];
 END
 
 let exc_located_wrapper f =
@@ -601,6 +606,9 @@ let parse_term stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+  
 
 (**/**)