From 4f6fd16c06b9e11bc2619a34c1629bd71aba76de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 15 Jun 2017 16:38:15 +0200
Subject: Remove the last use of the low-level Proof_type API in ssr.

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

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 490ded9d4..ded9fa66b 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -960,7 +960,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
           | _ -> assert false
       in loop sigma t [] n in
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t));
-    Refiner.refiner (Proof_type.Refine (EConstr.Unsafe.to_constr t)) gl
+    Tacmach.refine_no_check (EConstr.Unsafe.to_constr t) gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
   let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
-- 
cgit v1.2.3