hSqlite3.ml used create_fun_2 to define REGEXP.

[helm.git] / helm / software / components / tactics / tactics.ml

diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml
index 358de13038879ac647cd8e0c489cc3e3156c3d8e..527a8abb3bbb4b531a32bf95344ee767432ec2d1 100644 (file)
--- a/helm/software/components/tactics/tactics.ml
+++ b/helm/software/components/tactics/tactics.ml
@@ -29,7 +29,7 @@ let absurd = NegationTactics.absurd_tac
 let apply = PrimitiveTactics.apply_tac
 let applyS = Auto.applyS_tac
 let assumption = VariousTactics.assumption_tac
-let auto = AutoTactic.auto_tac
+let auto = Auto.auto_tac
 let cases_intros = PrimitiveTactics.cases_intros_tac
 let change = ReductionTactics.change_tac
 let clear = ProofEngineStructuralRules.clear
@@ -64,7 +64,6 @@ let rewrite = EqualityTactics.rewrite_tac
 let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
 let right = IntroductionTactics.right_tac
 let ring = Ring.ring_tac
-let set_goal = ProofEngineStructuralRules.set_goal
 let simpl = ReductionTactics.simpl_tac
 let split = IntroductionTactics.split_tac
 let subst = SubstTactic.subst_tac