type 'a localized_option =
LSome of 'a
- | LNone of Token.flocation
+ | LNone of GrafiteAst.loc
-type statement =
- include_paths:string list ->
- LexiconEngine.status ->
- LexiconEngine.status *
+type ast_statement =
(CicNotationPt.term, CicNotationPt.term,
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
- GrafiteAst.statement localized_option
+ GrafiteAst.statement
+
+type statement =
+ include_paths:string list ->
+ LexiconEngine.status ->
+ LexiconEngine.status * ast_statement localized_option
let grammar = CicNotationParser.level2_ast_grammar
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Change (loc, what, t)
- | IDENT "compare"; t = tactic_term ->
- GrafiteAst.Compare (loc,t)
| IDENT "constructor"; n = int ->
GrafiteAst.Constructor (loc, n)
| IDENT "contradiction" ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decide"; IDENT "equality" ->
- GrafiteAst.DecideEquality loc
| IDENT "decompose"; types = OPT ident_list0; what = IDENT;
(num, idents) = intros_spec ->
let types = match types with None -> [] | Some types -> types in
GrafiteAst.WMatch (loc,t)
| [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
GrafiteAst.WInstance (loc,t)
- | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT ->
+ | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
GrafiteAst.WLocate (loc,id)
| [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
GrafiteAst.WElim (loc, t)