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

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