* fold_tac has now a new parameter, which is the reduction to ``undo''

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

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 006471e9a961da81db2668a0a4e20d6542ff5bc6..710f8efacfad39a52c031fad2959f8d5730cd7b6 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -34,7 +34,8 @@ val perforate : Cic.context -> Cic.term -> Cic.term -> unit
 val whd : Cic.term -> unit
 val reduce : Cic.term -> unit
 val simpl : Cic.term -> unit
-val fold : Cic.term -> unit
+val fold_whd : Cic.term -> unit
+val fold_reduce : Cic.term -> unit
 
   (* scratch area reduction tactics *)
 val whd_in_scratch : Cic.term -> Cic.term -> Cic.term