New tactic rewrite implemented.

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 0e4de4f3bc1d639cadd821eaff0b535f5a1add99..0885f3037ffdcc1dfb9493ec1214f22f09b77022 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -273,4 +273,4 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
 let fourier () = apply_tactic FourierR.fourier_tac
-
+let rewrite term = apply_tactic (FourierR.rewrite_tac ~term)