]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
...
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 2efbc68115c35cc7ba4a74626ffcab92dae938de..d9c4608492dc9e02e6d664265ec2bfbfb9628d79 100644 (file)
@@ -82,6 +82,7 @@ let rec tactic_of_ast status ast =
   (* 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 ())