From 3f0438ba048b12ed626f0fb1ac421cc6df4b7d9f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 5 Sep 2008 18:40:08 +0000 Subject: [PATCH] we have to remove the Num directory :) --- .../contribs/procedural/Coq/Num/AddProps.mma | 54 ------------ .../contribs/procedural/Coq/Num/Axioms.mma | 76 ----------------- .../procedural/Coq/Num/Definitions.mma | 62 -------------- .../procedural/Coq/Num/DiscrAxioms.mma | 26 ------ .../procedural/Coq/Num/DiscrProps.mma | 26 ------ .../contribs/procedural/Coq/Num/EqAxioms.mma | 48 ----------- .../contribs/procedural/Coq/Num/EqParams.mma | 24 ------ .../contribs/procedural/Coq/Num/GeAxioms.mma | 30 ------- .../contribs/procedural/Coq/Num/GeProps.mma | 18 ---- .../contribs/procedural/Coq/Num/GtAxioms.mma | 30 ------- .../contribs/procedural/Coq/Num/GtProps.mma | 18 ---- .../contribs/procedural/Coq/Num/LeAxioms.mma | 30 ------- .../contribs/procedural/Coq/Num/LeProps.mma | 82 ------------------- .../procedural/Coq/Num/Leibniz/EqAxioms.mma | 48 ----------- .../procedural/Coq/Num/Leibniz/NSyntax.mma | 20 ----- .../procedural/Coq/Num/Leibniz/Params.mma | 54 ------------ .../contribs/procedural/Coq/Num/LtProps.mma | 72 ---------------- .../contribs/procedural/Coq/Num/NSyntax.mma | 20 ----- .../procedural/Coq/Num/Nat/Axioms.mma | 76 ----------------- .../procedural/Coq/Num/Nat/NSyntax.mma | 18 ---- .../procedural/Coq/Num/Nat/NeqDef.mma | 24 ------ .../contribs/procedural/Coq/Num/NeqAxioms.mma | 34 -------- .../contribs/procedural/Coq/Num/NeqDef.mma | 40 --------- .../contribs/procedural/Coq/Num/NeqParams.mma | 24 ------ .../contribs/procedural/Coq/Num/NeqProps.mma | 50 ----------- .../contribs/procedural/Coq/Num/OppAxioms.mma | 18 ---- .../contribs/procedural/Coq/Num/OppProps.mma | 18 ---- .../contribs/procedural/Coq/Num/Params.mma | 54 ------------ .../contribs/procedural/Coq/Num/SubProps.mma | 18 ---- 29 files changed, 1112 deletions(-) delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/Params.mma delete mode 100644 helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma diff --git a/helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma deleted file mode 100644 index 55be9ebf4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Axioms.ma". - -include "Num/EqAxioms.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_0.con ******************) - -inline procedural "cic:/Coq/Num/AddProps/add_x_0.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_Sy.con *****************) - -inline procedural "cic:/Coq/Num/AddProps/add_x_Sy.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_Sy_swap.con ************) - -inline procedural "cic:/Coq/Num/AddProps/add_x_Sy_swap.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_Sx_y_swap.con ************) - -inline procedural "cic:/Coq/Num/AddProps/add_Sx_y_swap.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_assoc_r.con **************) - -inline procedural "cic:/Coq/Num/AddProps/add_assoc_r.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_y_z_perm.con ***********) - -inline procedural "cic:/Coq/Num/AddProps/add_x_y_z_perm.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_one_S.con **************) - -inline procedural "cic:/Coq/Num/AddProps/add_x_one_S.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_one_x_S.con **************) - -inline procedural "cic:/Coq/Num/AddProps/add_one_x_S.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma deleted file mode 100644 index 895fde1dd..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma +++ /dev/null @@ -1,76 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -include "Num/EqParams.ma". - -include "Num/NSyntax.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/eq_refl.con ********************) - -inline procedural "cic:/Coq/Num/Axioms/eq_refl.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/eq_sym.con *********************) - -inline procedural "cic:/Coq/Num/Axioms/eq_sym.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/eq_trans.con *******************) - -inline procedural "cic:/Coq/Num/Axioms/eq_trans.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_sym.con ********************) - -inline procedural "cic:/Coq/Num/Axioms/add_sym.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_assoc_l.con ****************) - -inline procedural "cic:/Coq/Num/Axioms/add_assoc_l.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_0_x.con ********************) - -inline procedural "cic:/Coq/Num/Axioms/add_0_x.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_Sx_y.con *******************) - -inline procedural "cic:/Coq/Num/Axioms/add_Sx_y.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/S_0_1.con **********************) - -inline procedural "cic:/Coq/Num/Axioms/S_0_1.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_trans.con *******************) - -inline procedural "cic:/Coq/Num/Axioms/lt_trans.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_anti_refl.con ***************) - -inline procedural "cic:/Coq/Num/Axioms/lt_anti_refl.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_x_Sx.con ********************) - -inline procedural "cic:/Coq/Num/Axioms/lt_x_Sx.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_S_compat.con ****************) - -inline procedural "cic:/Coq/Num/Axioms/lt_S_compat.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_add_compat_l.con ************) - -inline procedural "cic:/Coq/Num/Axioms/lt_add_compat_l.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma b/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma deleted file mode 100644 index 76f648cf5..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma +++ /dev/null @@ -1,62 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/N.con *********************) - -inline procedural "cic:/Coq/Num/Definitions/N.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/zero.con ******************) - -inline procedural "cic:/Coq/Num/Definitions/zero.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/one.con *******************) - -inline procedural "cic:/Coq/Num/Definitions/one.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/add.con *******************) - -inline procedural "cic:/Coq/Num/Definitions/add.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/S.con *********************) - -inline procedural "cic:/Coq/Num/Definitions/S.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/eq.con ********************) - -inline procedural "cic:/Coq/Num/Definitions/eq.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/lt.con ********************) - -inline procedural "cic:/Coq/Num/Definitions/lt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/le.con ********************) - -inline procedural "cic:/Coq/Num/Definitions/le.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/gt.con ********************) - -inline procedural "cic:/Coq/Num/Definitions/gt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/ge.con ********************) - -inline procedural "cic:/Coq/Num/Definitions/ge.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/neq.con *******************) - -inline procedural "cic:/Coq/Num/Definitions/neq.con" as definition. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma deleted file mode 100644 index 665d67e16..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -include "Num/NSyntax.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/DiscrAxioms/lt_x_Sy_le.con ************) - -inline procedural "cic:/Coq/Num/DiscrAxioms/lt_x_Sy_le.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma deleted file mode 100644 index 2a1a6aa23..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/DiscrAxioms.ma". - -include "Num/LtProps.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/DiscrProps/lt_le_Sx_y.con *************) - -inline procedural "cic:/Coq/Num/DiscrProps/lt_le_Sx_y.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma deleted file mode 100644 index 49cadfe04..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -include "Num/EqParams.ma". - -include "Num/NSyntax.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/eq_refl.con ******************) - -inline procedural "cic:/Coq/Num/EqAxioms/eq_refl.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/eq_sym.con *******************) - -inline procedural "cic:/Coq/Num/EqAxioms/eq_sym.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/eq_trans.con *****************) - -inline procedural "cic:/Coq/Num/EqAxioms/eq_trans.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/add_eq_compat.con ************) - -inline procedural "cic:/Coq/Num/EqAxioms/add_eq_compat.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/S_eq_compat.con **************) - -inline procedural "cic:/Coq/Num/EqAxioms/S_eq_compat.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/lt_eq_compat.con *************) - -inline procedural "cic:/Coq/Num/EqAxioms/lt_eq_compat.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma b/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma deleted file mode 100644 index feea9e688..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqParams/eqN.con **********************) - -inline procedural "cic:/Coq/Num/EqParams/eqN.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma deleted file mode 100644 index c5d03cfe7..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Axioms.ma". - -include "Num/LtProps.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/not_lt_ge.con ****************) - -inline procedural "cic:/Coq/Num/GeAxioms/not_lt_ge.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/ge_not_lt.con ****************) - -inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma deleted file mode 100644 index ccc8303b4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma +++ /dev/null @@ -1,18 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma deleted file mode 100644 index c9dd783e6..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Axioms.ma". - -include "Num/LeProps.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/not_le_gt.con ****************) - -inline procedural "cic:/Coq/Num/GtAxioms/not_le_gt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/gt_not_le.con ****************) - -inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma deleted file mode 100644 index ccc8303b4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma +++ /dev/null @@ -1,18 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma deleted file mode 100644 index 181a2ddd1..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Axioms.ma". - -include "Num/LtProps.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeAxioms/lt_or_eq_le.con **************) - -inline procedural "cic:/Coq/Num/LeAxioms/lt_or_eq_le.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeAxioms/le_lt_or_eq.con **************) - -inline procedural "cic:/Coq/Num/LeAxioms/le_lt_or_eq.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma deleted file mode 100644 index 83e33fc15..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma +++ /dev/null @@ -1,82 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/LtProps.ma". - -include "Num/LeAxioms.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le.con *********************) - -inline procedural "cic:/Coq/Num/LeProps/lt_le.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/eq_le.con *********************) - -inline procedural "cic:/Coq/Num/LeProps/eq_le.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_eq_compat.con **************) - -inline procedural "cic:/Coq/Num/LeProps/le_eq_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_trans.con ******************) - -inline procedural "cic:/Coq/Num/LeProps/le_trans.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_l.con ***********) - -inline procedural "cic:/Coq/Num/LeProps/le_add_compat_l.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_r.con ***********) - -inline procedural "cic:/Coq/Num/LeProps/le_add_compat_r.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat.con *************) - -inline procedural "cic:/Coq/Num/LeProps/le_add_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_S_compat.con ***************) - -inline procedural "cic:/Coq/Num/LeProps/le_S_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_x_Sy.con ****************) - -inline procedural "cic:/Coq/Num/LeProps/le_lt_x_Sy.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_le_x_Sy.con ****************) - -inline procedural "cic:/Coq/Num/LeProps/le_le_x_Sy.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_Sx_y_lt.con ****************) - -inline procedural "cic:/Coq/Num/LeProps/le_Sx_y_lt.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le_trans.con ***************) - -inline procedural "cic:/Coq/Num/LeProps/lt_le_trans.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_trans.con ***************) - -inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con ******) - -inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con ******) - -inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma deleted file mode 100644 index 0693b7d97..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/NSyntax.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eqN.con **************) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eqN.con" as definition. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con **********) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con ***********) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con *********) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con ******) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con ****) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con *****) - -inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma deleted file mode 100644 index 83b4afc31..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma deleted file mode 100644 index b2d613740..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/N.con ******************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/N.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/zero.con ***************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/zero.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/one.con ****************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/one.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/add.con ****************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/add.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/S.con ******************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/S.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/lt.con *****************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/lt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/le.con *****************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/le.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/gt.con *****************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/gt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/ge.con *****************) - -inline procedural "cic:/Coq/Num/Leibniz/Params/ge.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma deleted file mode 100644 index b771e7af6..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma +++ /dev/null @@ -1,72 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Axioms.ma". - -include "Num/AddProps.ma". - -include "Num/NeqProps.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_anti_sym.con ***************) - -inline procedural "cic:/Coq/Num/LtProps/lt_anti_sym.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/eq_not_lt.con *****************) - -inline procedural "cic:/Coq/Num/LtProps/eq_not_lt.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_0_1.con ********************) - -inline procedural "cic:/Coq/Num/LtProps/lt_0_1.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/eq_lt_x_Sy.con ****************) - -inline procedural "cic:/Coq/Num/LtProps/eq_lt_x_Sy.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_lt_x_Sy.con ****************) - -inline procedural "cic:/Coq/Num/LtProps/lt_lt_x_Sy.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_Sx_y_lt.con ****************) - -inline procedural "cic:/Coq/Num/LtProps/lt_Sx_y_lt.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_neq.con ********************) - -inline procedural "cic:/Coq/Num/LtProps/lt_neq.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_neq_sym.con ****************) - -inline procedural "cic:/Coq/Num/LtProps/lt_neq_sym.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/neq_x_Sx.con ******************) - -inline procedural "cic:/Coq/Num/LtProps/neq_x_Sx.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/neq_0_1.con *******************) - -inline procedural "cic:/Coq/Num/LtProps/neq_0_1.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_add_compat_r.con ***********) - -inline procedural "cic:/Coq/Num/LtProps/lt_add_compat_r.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_add_compat.con *************) - -inline procedural "cic:/Coq/Num/LtProps/lt_add_compat.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma b/helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma deleted file mode 100644 index 83b4afc31..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma deleted file mode 100644 index 3f40a129c..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma +++ /dev/null @@ -1,76 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -include "Num/EqAxioms.ma". - -include "Num/NSyntax.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_Sx_y.con ***************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/add_Sx_y.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_0_x.con ****************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/add_0_x.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_sym.con ****************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/add_sym.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_eq_compat.con **********) - -inline procedural "cic:/Coq/Num/Nat/Axioms/add_eq_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_assoc_l.con ************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/add_assoc_l.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/S_0_1.con ******************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/S_0_1.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_trans.con ***************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_trans.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_x_Sx.con ****************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_x_Sx.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_S_compat.con ************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_S_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_eq_compat.con ***********) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_eq_compat.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_add_compat_l.con ********) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_add_compat_l.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_Sx_Sy_lt.con ************) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_Sx_Sy_lt.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_anti_refl.con ***********) - -inline procedural "cic:/Coq/Num/Nat/Axioms/lt_anti_refl.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma deleted file mode 100644 index ccc8303b4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma +++ /dev/null @@ -1,18 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma deleted file mode 100644 index 5d99d3db5..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/NeqDef/neq.con ********************) - -inline procedural "cic:/Coq/Num/Nat/NeqDef/neq.con" as definition. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma deleted file mode 100644 index d7ea7c81e..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma +++ /dev/null @@ -1,34 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/EqParams.ma". - -include "Num/NeqParams.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqAxioms/eq_not_neq.con **************) - -inline procedural "cic:/Coq/Num/NeqAxioms/eq_not_neq.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqAxioms/neq_sym.con *****************) - -inline procedural "cic:/Coq/Num/NeqAxioms/neq_sym.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqAxioms/neq_not_neq_trans.con *******) - -inline procedural "cic:/Coq/Num/NeqAxioms/neq_not_neq_trans.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma deleted file mode 100644 index b197e2993..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma +++ /dev/null @@ -1,40 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -include "Num/EqParams.ma". - -include "Num/EqAxioms.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq.con ************************) - -inline procedural "cic:/Coq/Num/NeqDef/neq.con" as definition. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/eq_not_neq.con *****************) - -inline procedural "cic:/Coq/Num/NeqDef/eq_not_neq.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq_sym.con ********************) - -inline procedural "cic:/Coq/Num/NeqDef/neq_sym.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq_not_neq_trans.con **********) - -inline procedural "cic:/Coq/Num/NeqDef/neq_not_neq_trans.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma deleted file mode 100644 index adc658df3..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/Params.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqParams/neq.con *********************) - -inline procedural "cic:/Coq/Num/NeqParams/neq.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma deleted file mode 100644 index c60ba32af..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma +++ /dev/null @@ -1,50 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -include "Num/NeqParams.ma". - -include "Num/NeqAxioms.ma". - -include "Num/EqParams.ma". - -include "Num/EqAxioms.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_antirefl.con *************) - -inline procedural "cic:/Coq/Num/NeqProps/neq_antirefl.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/eq_not_neq_y_x.con ***********) - -inline procedural "cic:/Coq/Num/NeqProps/eq_not_neq_y_x.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_not_eq.con ***************) - -inline procedural "cic:/Coq/Num/NeqProps/neq_not_eq.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_not_eq_y_x.con ***********) - -inline procedural "cic:/Coq/Num/NeqProps/neq_not_eq_y_x.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/not_neq_neq_trans.con ********) - -inline procedural "cic:/Coq/Num/NeqProps/not_neq_neq_trans.con" as lemma. - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_eq_compat.con ************) - -inline procedural "cic:/Coq/Num/NeqProps/neq_eq_compat.con" as lemma. - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma deleted file mode 100644 index ccc8303b4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma +++ /dev/null @@ -1,18 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma deleted file mode 100644 index ccc8303b4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma +++ /dev/null @@ -1,18 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Params.mma b/helm/software/matita/contribs/procedural/Coq/Num/Params.mma deleted file mode 100644 index 003da89e6..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/Params.mma +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/N.con **************************) - -inline procedural "cic:/Coq/Num/Params/N.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/zero.con ***********************) - -inline procedural "cic:/Coq/Num/Params/zero.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/one.con ************************) - -inline procedural "cic:/Coq/Num/Params/one.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/add.con ************************) - -inline procedural "cic:/Coq/Num/Params/add.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/S.con **************************) - -inline procedural "cic:/Coq/Num/Params/S.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/lt.con *************************) - -inline procedural "cic:/Coq/Num/Params/lt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/le.con *************************) - -inline procedural "cic:/Coq/Num/Params/le.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/gt.con *************************) - -inline procedural "cic:/Coq/Num/Params/gt.con". - -(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/ge.con *************************) - -inline procedural "cic:/Coq/Num/Params/ge.con". - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma deleted file mode 100644 index ccc8303b4..000000000 --- a/helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma +++ /dev/null @@ -1,18 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Coq.ma". - -- 2.39.2