From 61baf6f6422d60cd48dc7cf817f7d00ed8daae88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 8 Dec 2018 18:51:43 +0100
Subject: [rtauto] [auto] Use new proof engine.

---
 plugins/rtauto/g_rtauto.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/rtauto/g_rtauto.mlg')

diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg
index 9c9fdcfa2f..d8724eb976 100644
--- a/plugins/rtauto/g_rtauto.mlg
+++ b/plugins/rtauto/g_rtauto.mlg
@@ -17,6 +17,6 @@ open Ltac_plugin
 DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
-| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) }
+| [ "rtauto" ] -> { Refl_tauto.rtauto_tac }
 END
 
-- 
cgit v1.2.3