From 654b69cbeb55a0cab3c2328d73355ad2510d1a85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Oct 2015 14:21:25 +0100
Subject: Fixing another instance of bug #3267 in eauto, this time in the
 presence of hints modifying the context and of a "using" clause.

Incidentally opening Hints by default in debugger.
---
 dev/base_include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index d58b6ad13c..dac1f6093c 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -148,6 +148,7 @@ open Tactic_debug
 open Decl_proof_instr
 open Decl_mode
 
+open Hints
 open Auto
 open Autorewrite
 open Contradiction
-- 
cgit v1.2.3