we have to remove the Num directory :)

[helm.git] / helm / software / matita / contribs / procedural / Coq / Num / Nat / Axioms.mma

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.
-