New tactic rewrite implemented.

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

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