From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 plugins/ltac/g_rewrite.ml4 | 1 -
 plugins/ltac/rewrite.ml    | 1 -
 2 files changed, 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fdcaedab3a..ac979bcf89 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,6 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Tacticals
 open Proofview.Notations
 open Rewrite
 open Stdarg
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9a1615d3f2..5630a2d7b6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Reduction
 open Tacticals.New
-open Tacmach
 open Tactics
 open Pretype_errors
 open Typeclasses
-- 
cgit v1.2.3