let composites = match composites with None -> true | Some _ -> false in
GrafiteAst.Coercion
(loc, t, composites, arity, saturations)
+ | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
+ GrafiteAst.PreferCoercion (loc, t)
| IDENT "unification"; IDENT "hint"; t = tactic_term ->
GrafiteAst.UnificationHint (loc, t)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->