From ffda464321e856e44c7f99e6aab201770781c806 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 May 2020 19:04:11 +0200
Subject: Remove call to Refiner API from Funind.

---
 plugins/funind/recdef.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/recdef.ml')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ffb9a7e69b..7b4316c523 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g =
   in
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
 
-let pf_type c tac gl =
-  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
-  tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_type c tac =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let evars, ty = Typing.type_of env sigma c in
+      tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty))
+
+let pf_type c tac =
+  Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty)))
 
 let pf_typel l tac =
   let rec aux tys l =
-- 
cgit v1.2.3