From 417641e48129c9ba8656c622c9b64cd32641e7de Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Nov 2018 20:16:41 +0100
Subject: [legacy proof engine] Remove some cruft.

We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.

This is not a lot but every little step helps.
---
 plugins/funind/functional_principles_proofs.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 92fa94d6dc..ef1d1af199 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -131,8 +131,7 @@ let finish_proof dynamic_infos g =
     g
 
 
-let refine c =
-  Tacmach.refine c
+let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
 
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 
-- 
cgit v1.2.3