Signature and concrete syntax of fold fixed.

[helm.git] / helm / ocaml / tactics / tactics.mli

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 187dc2be3b4725e70cf9b8f376ea90bbb562533a..c155d67d39adecb386a861e47bdec3f01f4f492e 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -33,6 +33,7 @@ val exists : ProofEngineTypes.tactic
 val fail : ProofEngineTypes.tactic
 val fold :
   reduction:(Cic.context -> Cic.term -> Cic.term) ->
+  term:Cic.term ->
   pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val fourier : ProofEngineTypes.tactic
 val fwd_simpl :