GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
+ | IDENT "applyP"; t = tactic_term ->
+ GrafiteAst.ApplyP (loc, t)
| IDENT "applyS"; t = tactic_term ; params = auto_params ->
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
| [ IDENT "theorem" ] -> `Theorem
]
];
+ inline_flavour: [
+ [ attr = theorem_flavour -> attr
+ | [ IDENT "axiom" ] -> `Axiom
+ | [ IDENT "mutual" ] -> `MutualDefinition
+ ]
+ ];
inductive_spec: [ [
fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
GrafiteAst.Check (loc, t)
| [ IDENT "inline"];
style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
- suri = QSTRING; prefix = OPT QSTRING ->
+ suri = QSTRING; prefix = OPT QSTRING;
+ flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
let style = match style with
| None -> GrafiteAst.Declarative
| Some depth -> GrafiteAst.Procedural depth
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
- GrafiteAst.Inline (loc,style,suri,prefix)
+ GrafiteAst.Inline (loc,style,suri,prefix, flavour)
| [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
| IDENT "auto"; params = auto_params ->
let alpha = "[a-zA-Z]" in
let num = "[0-9]+" in
let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
- let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
+ let decoration = "\\'" in
+ let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
let rex = Str.regexp ("^"^ident^"$") in
if Str.string_match rex id 0 then
if (try ignore (UriManager.uri_of_string uri); true