X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FNPlus%2Fdefs.ma;h=34f4e3491eba32b2d3620690eda0ebf2e4a8d300;hb=3999b3279443c7d106812d8930dfced8d8bc37dc;hp=93c7a2e45f1da1926dde81919da068133c482b8c;hpb=092d5c718ea90255ce1009acd5aa0942e4449898;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma
index 93c7a2e45..34f4e3491 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs".
 
-include "datatypes/defs.ma".
+
+include "datatypes/Nat.ma".
 
 inductive NPlus (p:Nat): Nat \to Nat \to Prop \def
    | nplus_zero_2: NPlus p zero p