From 85c509a0fada387d3af96add3dac6a7c702b5d01 Mon Sep 17 00:00:00 2001
From: letouzey
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/proof_search.ml | 10 ----------
 plugins/rtauto/refl_tauto.ml   |  9 ---------
 2 files changed, 19 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d1ba173d3f..20ec172697 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Errors
 open Util
 open Goptions
@@ -63,15 +62,6 @@ type form=
   | Conjunct of form * form
   | Disjunct of form * form
 
-type tag=int
-
-let decomp_form=function
-    Atom i -> Some (i,[])
-  | Arrow (f1,f2) -> Some (-1,[f1;f2])
-  | Bot -> Some (-2,[])
-  | Conjunct (f1,f2) -> Some (-3,[f1;f2])
-  | Disjunct (f1,f2) -> Some (-4,[f1;f2])
-
 module Fmap=Map.Make(struct type t=form let compare=compare end)
 
 type sequent =
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index c10aece996..ceaf2a79be 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