New tactic unfold.

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index 02e56ba6a207224e38bfa479673f8f01372df2d0..ebb61a7c8bbb54ccf0094d050dfd8cdd8dc8a3a8 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -46,3 +46,4 @@ val replace_lifting_csc :
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term
+val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term