| GrafiteAst.Clear (_,id) -> Tactics.clear id
| GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
| GrafiteAst.Contradiction _ -> Tactics.contradiction
- | GrafiteAst.Compare (_, term) -> Tactics.compare term
| GrafiteAst.Constructor (_, n) -> Tactics.constructor n
| GrafiteAst.Cut (_, ident, term) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
| GrafiteAst.Decompose (_, types, what, names) ->
let to_type = function
| GrafiteAst.Type (uri, typeno) -> uri, typeno