tactic: [
[ IDENT "absurd"; t = tactic_term ->
GrafiteAst.Absurd (loc, t)
+ | IDENT "apply"; IDENT "rule"; t = tactic_term ->
+ GrafiteAst.ApplyRule (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
| IDENT "applyP"; t = tactic_term ->
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
+ | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
+ GrafiteAst.Eval (loc, kind, t)
| [ IDENT "inline"];
style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
suri = QSTRING; prefix = OPT QSTRING;
let composites = match composites with None -> true | Some _ -> false in
GrafiteAst.Coercion
(loc, t, composites, arity, saturations)
+ | IDENT "unification"; IDENT "hint"; t = tactic_term ->
+ GrafiteAst.UnificationHint (loc, t)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
[ ex = executable ->
fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
| com = comment ->
- fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+ fun ?(never_include=false) ~include_paths status ->
+ status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
!out fname;
fun ?(never_include=false) ~include_paths status ->