From e824d429363262a9ff9db117282fe15289b5ab59 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Oct 2014 15:15:58 +0200
Subject: A version of convert_concl and convert_hyp in new proof engine.

Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
---
 plugins/quote/quote.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index ed7f180014..64166a0de6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -457,8 +457,8 @@ let quote f lid =
       | _ -> assert false
     in
     match ivs.variable_lhs with
-    | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
-    | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
   end
 
 let gen_quote cont c f lid =
-- 
cgit v1.2.3