X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.mli;h=f5c31067f8f44ce5adaa19f0e64861e7a27b7986;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=fed8d04ad7598a6689625c3acf740a0f3373c55b;hpb=d5c0d882413668e6569df55f501efe92cf3bf100;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index fed8d04ad..f5c31067f 100644
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -58,3 +58,4 @@ val clear : Cic.hypothesis -> unit
 val elim_type : Cic.term -> unit
 val ring : unit -> unit
 val fourier : unit -> unit
+val rewrite_simpl : Cic.term -> unit