From 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 14 Sep 2012 15:59:23 +0000
Subject: This patch removes unused "open" (automatically generated from
 compiler warnings).

I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/cc/ccalgo.ml  | 1 -
 plugins/cc/ccproof.ml | 1 -
 plugins/cc/cctac.ml   | 5 -----
 3 files changed, 7 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 0970717edd..8af15a1d57 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -17,7 +17,6 @@ open Names
 open Term
 open Tacmach
 open Evd
-open Proof_type
 
 let init_size=5
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index d5eab32c4f..25c01f2bd3 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
-open Util
 open Names
 open Term
 open Ccalgo
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2042f9b058..53c146bfce 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -9,10 +9,7 @@
 (* This file is the interface between the c-c algorithm and Coq *)
 
 open Evd
-open Proof_type
 open Names
-open Libnames
-open Nameops
 open Inductiveops
 open Declarations
 open Term
@@ -21,12 +18,10 @@ open Tactics
 open Tacticals
 open Typing
 open Ccalgo
-open Tacinterp
 open Ccproof
 open Pp
 open Errors
 open Util
-open Format
 
 let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
-- 
cgit v1.2.3