we have to remove the Num directory :)

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 (file)
index 55be9eb..0000000
--- 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 (file)
index 895fde1..0000000
--- 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 (file)
index 76f648c..0000000
--- 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 (file)
index 665d67e..0000000
--- 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 (file)
index 2a1a6aa..0000000
--- 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 (file)
index 49cadfe..0000000
--- 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 (file)
index feea9e6..0000000
--- 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 (file)
index c5d03cf..0000000
--- 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 (file)
index ccc8303..0000000
--- 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 (file)
index c9dd783..0000000
--- 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 (file)
index ccc8303..0000000
--- 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 (file)
index 181a2dd..0000000
--- 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 (file)
index 83e33fc..0000000
--- 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 (file)
index 0693b7d..0000000
--- 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 (file)
index 83b4afc..0000000
--- 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 (file)
index b2d6137..0000000
--- 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 (file)
index b771e7a..0000000
--- 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 (file)
index 83b4afc..0000000
--- 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 (file)
index 3f40a12..0000000
--- 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 (file)
index ccc8303..0000000
--- 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 (file)
index 5d99d3d..0000000
--- 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 (file)
index d7ea7c8..0000000
--- 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 (file)
index b197e29..0000000
--- 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 (file)
index adc658d..0000000
--- 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 (file)
index c60ba32..0000000
--- 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 (file)
index ccc8303..0000000
--- 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 (file)
index ccc8303..0000000
--- 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 (file)
index 003da89..0000000
--- 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 (file)
index ccc8303..0000000
--- 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".
-