- rewritesimpl_tac added in fourierR.ml (wrong location)

[helm.git] / helm / gTopLevel / proofEngine.mli

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index a11914a9ae7dc4a0517e4248b8772f0cc89add76..f5c31067f8f44ce5adaa19f0e64861e7a27b7986 100644 (file)
--- 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