From a76a71eda10b054b04de4ff56f0637a32077edd4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 18:09:30 +0200
Subject: Remove two unused opens.

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

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3c430cb174..2d54b61c72 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -9,8 +9,6 @@
 open Equality
 open Names
 open Pp
-open Tacticals
-open Tactics
 open Term
 open Termops
 open CErrors
-- 
cgit v1.2.3