From 874ff85e2d52b33010007bb3a1f1add9391b030f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 2 May 2017 16:33:59 +0200
Subject: Remove unused module definition after merging PR#592.

---
 tactics/hints.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index d57e4875c1..c5bacc5a20 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open Util
 open CErrors
-- 
cgit v1.2.3