(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyRule (_, term) -> Tactics.apply term
| 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
- let is_record = function `Class (`Record att) -> Some att | _-> None in
+ let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in
match HExtlib.list_findopt is_record attributes with
| None -> status,[]
| Some fields ->