From 5549be611f33cb52e4725e65b7f9603de22de863 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Nov 2004 10:10:52 +0000 Subject: [PATCH] Porting to the new version of auto. --- helm/gTopLevel/proofEngine.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 25f81e37b..ac1119dd5 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -227,7 +227,10 @@ let fold_simpl term = let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac -let auto ~dbd () = apply_tactic (VariousTactics.auto_tac ~dbd) + +(* let auto ~dbd () = apply_tactic (AutoTactic.auto_tac ~dbd) *) +let auto ~dbd () = apply_tactic (AutoTactic.auto_tac_new ~dbd) + let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term) let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term) -- 2.39.2