(* 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 ())
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
* 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