From 85c509a0fada387d3af96add3dac6a7c702b5d01 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 2 Oct 2012 15:58:00 +0000
Subject: Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/rtauto/refl_tauto.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'plugins/rtauto/refl_tauto.ml')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index c10aece99..ceaf2a79b 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -11,8 +11,6 @@ module Search = Explore.Make(Proof_search)
 open Errors
 open Util
 open Term
-open Names
-open Evd
 open Tacmach
 open Proof_search
 
@@ -29,13 +27,6 @@ let li_False = lazy (destInd (logic_constant "False"))
 let li_and = lazy (destInd (logic_constant "and"))
 let li_or =  lazy (destInd (logic_constant "or"))
 
-let data_constant =
-  Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"]
-
-let l_true_equals_true =
-  lazy (mkApp(logic_constant "eq_refl",
-        [|data_constant "bool";data_constant "true"|]))
-
 let pos_constant =
   Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
 
-- 
cgit v1.2.3