From a33f772631696c694f0d9a7fad3a914037c464b2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:56:26 +0200
Subject: Refining out the Refiner.

---
 dev/base_include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 67ea3a1fa1..1f14fc2941 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -114,7 +114,6 @@ open Logic
 open Proof
 open Proof_using
 open Redexpr
-open Refiner
 open Tacmach
 
 open Hints
-- 
cgit v1.2.3