X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=c29babd55414b1fd3b1d7b75e23f3ebdb6eadf60;hp=c4ec503c797a2418b66ea0dcfc8c39359f747b80;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hpb=9ab5bcc58aa62e4ded71fd64cc5a4ea562195103

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index c4ec503c7..c29babd55 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -85,6 +85,7 @@ type ntactic =
    justification, conclusion, identifier, eqconcl *)
    | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
    identifier, equivnewcon *)
+   | BetaRewritingStep of loc * nterm
    | Bydone of loc * just
    | ExistsElim of loc * just * string * nterm * nterm * string
    | AndElim of loc * just * nterm * string * nterm * string