diff options
| author | Pierre-Marie Pédrot | 2018-10-17 15:24:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-17 15:24:51 +0200 |
| commit | 063cf49f40511730c8c60c45332e92823ce4c78f (patch) | |
| tree | 634499887282859174f32e2ac3f61d2d97b0fd2d /plugins/btauto | |
| parent | f111af975860b5f48bb792d718e4eb211f6fa57f (diff) | |
| parent | 7af4bcb7003d4f02542834930ad0da1e83c5ff0c (diff) | |
Merge PR #8710: [omega, btauto] Remove some 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 |