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

---
 plugins/firstorder/rules.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e676a8a936..d539eda579 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -210,6 +210,6 @@ let defined_connectives=lazy
 let normalize_evaluables=
   onAllHypsAndConcl
     (function
-	 None->unfold_in_concl (Lazy.force defined_connectives)
+	 None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
        | Some id ->
-	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+	   Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
-- 
cgit v1.2.3