From 5ac88949f0fbab1f47781c9de4edbcffa19d9896 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:35:15 +0000
Subject: Removes Refine from the dev tools now that the module has been
 deleted.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16979 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 ca40f5f7af..87c0e5b7e9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -140,7 +140,6 @@ open Hiddentac
 open Hipattern
 open Inv
 open Leminv
-open Refine
 open Tacsubst
 open Tacintern
 open Tacinterp
-- 
cgit v1.2.3