]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
aliases removed
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index ac63812461ab3002c9eb4ee5e2a4c42f9ce7ef6c..4a92548454f56366c9e0dc357d277b2f3d9d5bd0 100644 (file)
@@ -152,7 +152,7 @@ let tactic_of_ast ast =
   | GrafiteAst.Right _ -> Tactics.right
   | GrafiteAst.Ring _ -> Tactics.ring
   | GrafiteAst.Split _ -> Tactics.split
-  | GrafiteAst.Subst (_, hyp) -> Tactics.subst ~hyp
+  | GrafiteAst.Subst _ -> Tactics.subst
   | GrafiteAst.Symmetry _ -> Tactics.symmetry
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
   (* Implementazioni Aggiunte *)