From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 plugins/ltac/rewrite.ml | 2 +-
 plugins/ltac/tauto.ml   | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 12a1566e20..9a1615d3f2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -39,7 +39,7 @@ open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 
 (** Typeclass-based generalized rewriting. *)
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index e86d1c7283..4de2081cf8 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -10,7 +10,6 @@ open Term
 open EConstr
 open Hipattern
 open Names
-open Pp
 open Geninterp
 open Misctypes
 open Tacexpr
-- 
cgit v1.2.3