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)
vars body
EXTEND
- GLOBAL: term term0 statement;
+ GLOBAL: term term0 statement statements;
int: [
[ num = NUM ->
try
| com = comment -> TacticAst.Comment (loc, com)
]
];
+ statements: [
+ [ l = LIST0 [ statement ] -> l
+ ]
+ ];
END
let exc_located_wrapper f =
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))
+
(**/**)