From 5548e5f6bc5446f7541cfc7d93b0b47e4b751e86 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 15:39:17 +0200
Subject: Remove unused open.

---
 tactics/eqdecide.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 472cd8f22b..641929a77b 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -67,7 +67,6 @@ let choose_noteq eqonleft =
     left_with_bindings false Misctypes.NoBindings
 
 open Sigma.Notations
-open Context.Rel.Declaration
 
 (* A surgical generalize which selects the right occurrences by hand *)
 (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
-- 
cgit v1.2.3