From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 vernac/auto_ind_decl.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'vernac/auto_ind_decl.ml')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 015552d68..25091f783 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -9,7 +9,6 @@
 (* This file is about the automatic generation of schemes about
    decidable equality, created by Vincent Siles, Oct 2007 *)
 
-open Tacmach
 open CErrors
 open Util
 open Pp
@@ -716,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec =
         ))), eff
 
 let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
-  let open EConstr in
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
-- 
cgit v1.2.3