debian release 0.0.4-2:

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

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index fed8d04ad7598a6689625c3acf740a0f3373c55b..f5c31067f8f44ce5adaa19f0e64861e7a27b7986 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_simpl : Cic.term -> unit