GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
- (num, idents) = intros_spec ->
+ ispecs = intros_spec ->
let pattern = match pattern with
| None -> None, [], Some Ast.UserInput
| Some pattern -> pattern
in
- GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
+ GrafiteAst.Elim (loc, what, using, pattern, ispecs)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, (num, idents))
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 "prefer" ; IDENT "coercion"; t = tactic_term ->
+ GrafiteAst.PreferCoercion (loc, t)
+ | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+ GrafiteAst.UnificationHint (loc, t, n)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->