let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
- | IDENT "destruct"; t = tactic_term ->
- GrafiteAst.Destruct (loc, t)
+ | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+ GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
GrafiteAst.Ring loc
| IDENT "split" ->
GrafiteAst.Split loc
- | IDENT "subst" ->
- GrafiteAst.Subst loc
| IDENT "symmetry" ->
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
- | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+ | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
+ if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
| IDENT "auto"; params = auto_params ->
GrafiteAst.AutoInteractive (loc,params)
| [ IDENT "whelp"; "match" ] ; t = term ->
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+ | IDENT "coercion" ; suri = URI ; arity = OPT int ;
+ saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
let arity = match arity with None -> 0 | Some x -> x in
- GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+ let saturations = match saturations with None -> 0 | Some x -> x in
+ let composites = match composites with None -> true | Some _ -> false in
+ GrafiteAst.Coercion
+ (loc, UriManager.uri_of_string suri, composites, arity, saturations)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->