From d5fece25d8964d5d9fcd55b66164286aeef5fb9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Aug 2014 20:44:03 +0200
Subject: Reorganization of tactics: - made "apply" tactics of type
 Proofview.tactic, as well as other inner   functions about elim and assert -
 used same hypothesis naming policy for intros and internal_cut (towards a  
 reorganization of intro patterns) - "apply ... in H as pat" now supports any
 kind of introduction   pattern (doc not changed)

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

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index dbd89019e2..e6a8411534 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -248,7 +248,7 @@ module Btauto = struct
           let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
           Tacticals.New.tclTHENLIST [
             Proofview.V82.tactic (Tactics.change_concl changed_gl);
-            Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
+            Tactics.apply (Lazy.force soundness);
             Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
             try_unification env
           ]
-- 
cgit v1.2.3