X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftactics.ml;h=527a8abb3bbb4b531a32bf95344ee767432ec2d1;hb=cebed8851dcaf8ceeb4e5f74b52705bf0c18a456;hp=fc1d4b7a3a1c33960f265b0e9cf969b422efc107;hpb=50afaf262195266d156f594cff7e92a6e8898b3e;p=helm.git diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index fc1d4b7a3..527a8abb3 100644 --- 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