(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
| GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
| GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
* information inside the moo *)
let add_coercions_of_record_to_moo obj lemmas status =
let attributes = CicUtil.attributes_of_obj obj in
* information inside the moo *)
let add_coercions_of_record_to_moo obj lemmas status =
let attributes = CicUtil.attributes_of_obj obj in