ocaml 3.09 transition

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

diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml
index 055c00528139b5defa52843582d2e7b1a8d5dbec..e75677caf9253fe0dd282a68927359ceb8674316 100644 (file)
--- a/helm/ocaml/tactics/tactics.ml
+++ b/helm/ocaml/tactics/tactics.ml
@@ -27,7 +27,7 @@ let absurd = NegationTactics.absurd_tac
 let apply = PrimitiveTactics.apply_tac
 let assumption = VariousTactics.assumption_tac
 let auto = AutoTactic.auto_tac
-let change = PrimitiveTactics.change_tac
+let change = ReductionTactics.change_tac
 let clear = ProofEngineStructuralRules.clear
 let clearbody = ProofEngineStructuralRules.clearbody
 let compare = DiscriminationTactics.compare_tac
@@ -66,4 +66,5 @@ let simpl = ReductionTactics.simpl_tac
 let split = IntroductionTactics.split_tac
 let symmetry = EqualityTactics.symmetry_tac
 let transitivity = EqualityTactics.transitivity_tac
+let unfold = ReductionTactics.unfold_tac
 let whd = ReductionTactics.whd_tac