From 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 15 Feb 2016 14:26:43 +0100
Subject: Moving conversion functions to the new tactic API.

---
 plugins/btauto/refl_btauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/btauto/refl_btauto.ml')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 5a49fc8f4..57eb80f5f 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -250,7 +250,7 @@ module Btauto = struct
           Tacticals.New.tclTHENLIST [
             Tactics.change_concl changed_gl;
             Tactics.apply (Lazy.force soundness);
-            Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
+            Tactics.normalise_vm_in_concl;
             try_unification env
           ]
       | _ ->
-- 
cgit v1.2.3