From 8bba1951cab1088d057aac68425271191b7c296c Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 11 Oct 2018 13:04:24 +0000
Subject: [btauto] Remove dead code

---
 plugins/btauto/refl_btauto.ml  |  5 -----
 plugins/btauto/refl_btauto.mli | 11 +++++++++++
 2 files changed, 11 insertions(+), 5 deletions(-)
 create mode 100644 plugins/btauto/refl_btauto.mli

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index ac0a875229..b9ad1ff6d8 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -10,8 +10,6 @@
 
 open Constr
 
-let contrib_name = "btauto"
-
 let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n)
 
 let decomp_term sigma (c : Constr.t) =
@@ -23,7 +21,6 @@ let (===) = Constr.equal
 
 
 module CoqList = struct
-  let typ  =  bt_lib_constr "core.list.type"
   let _nil =  bt_lib_constr "core.list.nil"
   let _cons = bt_lib_constr "core.list.cons"
 
@@ -32,12 +29,10 @@ module CoqList = struct
   let rec of_list ty = function
     | [] -> nil ty
     | t::q -> cons ty t (of_list ty q)
-  let type_of_list ty = lapp typ [|ty|]
 
 end
 
 module CoqPositive = struct
-  let typ = bt_lib_constr "num.pos.type"
   let _xH = bt_lib_constr "num.pos.xH"
   let _xO = bt_lib_constr "num.pos.xO"
   let _xI = bt_lib_constr "num.pos.xI"
diff --git a/plugins/btauto/refl_btauto.mli b/plugins/btauto/refl_btauto.mli
new file mode 100644
index 0000000000..5478fddba5
--- /dev/null
+++ b/plugins/btauto/refl_btauto.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module Btauto : sig val tac : unit Proofview.tactic end
-- 
cgit v1.2.3