diff options
| author | Vincent Laporte | 2018-10-11 13:04:24 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-16 12:03:50 +0000 |
| commit | 8bba1951cab1088d057aac68425271191b7c296c (patch) | |
| tree | ca4ac7edce79bab084f9acb6fe5d4015a24a0cbc /plugins/btauto | |
| parent | 62edc7839bb4b534ea0e82d4ed36f504ad04cb16 (diff) | |
[btauto] Remove dead code
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 5 | ||||
| -rw-r--r-- | plugins/btauto/refl_btauto.mli | 11 |
2 files changed, 11 insertions, 5 deletions
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 |