From c86f1a6c4d00f66a81c576589f215cb667595710 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 23 Aug 2006 08:04:36 +0000
Subject: [PATCH] new naming

---
 matita/contribs/RELATIONAL/BEq/{BEq.ma => defs.ma}            | 2 +-
 matita/contribs/RELATIONAL/BNot/{BNot.ma => defs.ma}          | 2 +-
 matita/contribs/RELATIONAL/Bool/{Bool.ma => defs.ma}          | 0
 matita/contribs/RELATIONAL/NLE/{NLE.ma => defs.ma}            | 2 +-
 matita/contribs/RELATIONAL/NPlus/{NPlus.ma => defs.ma}        | 2 +-
 matita/contribs/RELATIONAL/NPlus/{NPlus_fwd.ma => fwd.ma}     | 4 ++--
 matita/contribs/RELATIONAL/NPlus/{NPlus_props.ma => props.ma} | 2 +-
 matita/contribs/RELATIONAL/Nat/{Nat.ma => defs.ma}            | 0
 matita/contribs/RELATIONAL/Nat/{Nat_fwd.ma => fwd.ma}         | 2 +-
 9 files changed, 8 insertions(+), 8 deletions(-)
 rename matita/contribs/RELATIONAL/BEq/{BEq.ma => defs.ma} (98%)
 rename matita/contribs/RELATIONAL/BNot/{BNot.ma => defs.ma} (97%)
 rename matita/contribs/RELATIONAL/Bool/{Bool.ma => defs.ma} (100%)
 rename matita/contribs/RELATIONAL/NLE/{NLE.ma => defs.ma} (98%)
 rename matita/contribs/RELATIONAL/NPlus/{NPlus.ma => defs.ma} (98%)
 rename matita/contribs/RELATIONAL/NPlus/{NPlus_fwd.ma => fwd.ma} (98%)
 rename matita/contribs/RELATIONAL/NPlus/{NPlus_props.ma => props.ma} (99%)
 rename matita/contribs/RELATIONAL/Nat/{Nat.ma => defs.ma} (100%)
 rename matita/contribs/RELATIONAL/Nat/{Nat_fwd.ma => fwd.ma} (98%)

diff --git a/matita/contribs/RELATIONAL/BEq/BEq.ma b/matita/contribs/RELATIONAL/BEq/defs.ma
similarity index 98%
rename from matita/contribs/RELATIONAL/BEq/BEq.ma
rename to matita/contribs/RELATIONAL/BEq/defs.ma
index 3d40598f0..0b52af116 100644
--- a/matita/contribs/RELATIONAL/BEq/BEq.ma
+++ b/matita/contribs/RELATIONAL/BEq/defs.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/BEq/defs".
 
 include "logic/equality.ma".
 
-include "BNot/BNot.ma".
+include "BNot/defs.ma".
 
 inductive BEq (b1:Bool): Bool \to Bool \to Prop \def
    | beq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2
diff --git a/matita/contribs/RELATIONAL/BNot/BNot.ma b/matita/contribs/RELATIONAL/BNot/defs.ma
similarity index 97%
rename from matita/contribs/RELATIONAL/BNot/BNot.ma
rename to matita/contribs/RELATIONAL/BNot/defs.ma
index f83a3c8ca..d62264513 100644
--- a/matita/contribs/RELATIONAL/BNot/BNot.ma
+++ b/matita/contribs/RELATIONAL/BNot/defs.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/BNot/defs".
 
-include "Bool/Bool.ma".
+include "Bool/defs.ma".
 
 inductive BNot: Bool \to Bool \to Prop \def
    | bnot_false: BNot false true
diff --git a/matita/contribs/RELATIONAL/Bool/Bool.ma b/matita/contribs/RELATIONAL/Bool/defs.ma
similarity index 100%
rename from matita/contribs/RELATIONAL/Bool/Bool.ma
rename to matita/contribs/RELATIONAL/Bool/defs.ma
diff --git a/matita/contribs/RELATIONAL/NLE/NLE.ma b/matita/contribs/RELATIONAL/NLE/defs.ma
similarity index 98%
rename from matita/contribs/RELATIONAL/NLE/NLE.ma
rename to matita/contribs/RELATIONAL/NLE/defs.ma
index 29d15e2ab..19e45c3bc 100644
--- a/matita/contribs/RELATIONAL/NLE/NLE.ma
+++ b/matita/contribs/RELATIONAL/NLE/defs.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NLE/defs".
 
-include "Nat/Nat.ma".
+include "Nat/defs.ma".
 
 inductive NLE: Nat \to Nat \to Prop \def
    | NLE_zero: \forall q. NLE zero q
diff --git a/matita/contribs/RELATIONAL/NPlus/NPlus.ma b/matita/contribs/RELATIONAL/NPlus/defs.ma
similarity index 98%
rename from matita/contribs/RELATIONAL/NPlus/NPlus.ma
rename to matita/contribs/RELATIONAL/NPlus/defs.ma
index 271bce10b..92561bc5c 100644
--- a/matita/contribs/RELATIONAL/NPlus/NPlus.ma
+++ b/matita/contribs/RELATIONAL/NPlus/defs.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs".
 
 include "logic/equality.ma".
 
-include "Nat/Nat.ma".
+include "Nat/defs.ma".
 
 inductive NPlus (p:Nat): Nat \to Nat \to Prop \def
    | nplus_zero_2: NPlus p zero p
diff --git a/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma
similarity index 98%
rename from matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma
rename to matita/contribs/RELATIONAL/NPlus/fwd.ma
index d6de420e2..bae48d405 100644
--- a/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NPlus/fwd".
 
-include "Nat/Nat_fwd.ma".
-include "NPlus/NPlus.ma".
+include "Nat/fwd.ma".
+include "NPlus/defs.ma".
 
 (* primitive generation lemmas proved by elimination and inversion *)
 
diff --git a/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma
similarity index 99%
rename from matita/contribs/RELATIONAL/NPlus/NPlus_props.ma
rename to matita/contribs/RELATIONAL/NPlus/props.ma
index eb580c983..56146a3bf 100644
--- a/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma
+++ b/matita/contribs/RELATIONAL/NPlus/props.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NPlus/props".
 
-include "NPlus/NPlus_fwd.ma".
+include "NPlus/fwd.ma".
 
 theorem nplus_zero_1: \forall q. NPlus zero q q.
  intros. elim q; clear q; auto.
diff --git a/matita/contribs/RELATIONAL/Nat/Nat.ma b/matita/contribs/RELATIONAL/Nat/defs.ma
similarity index 100%
rename from matita/contribs/RELATIONAL/Nat/Nat.ma
rename to matita/contribs/RELATIONAL/Nat/defs.ma
diff --git a/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma b/matita/contribs/RELATIONAL/Nat/fwd.ma
similarity index 98%
rename from matita/contribs/RELATIONAL/Nat/Nat_fwd.ma
rename to matita/contribs/RELATIONAL/Nat/fwd.ma
index 28c8733cb..09847de2e 100644
--- a/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma
+++ b/matita/contribs/RELATIONAL/Nat/fwd.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/Nat/fwd".
 
 include "logic/equality.ma".
 
-include "Nat/Nat.ma".
+include "Nat/defs.ma".
 
 theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P.
  intros. discriminate H.
-- 
2.39.2