better type for comparison and implementation of KBO orderings

[helm.git] / helm / software / matita / tests / depends

diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index e2adc110683f00ef9f54ca9e2df52de8bc893f26..0a676a77c77ebda4a986d6d1129427c9dfd60494 100644 (file)
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -78,7 +78,7 @@ TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
 TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
 TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
 bool.ma coq.ma
-ng_tactics.ma logic/connectives.ma nat/plus.ma
+ng_tactics.ma logic/connectives.ma nat/plus.ma ng_pts.ma
 TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
 TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
@@ -92,6 +92,7 @@ continuationals.ma coq.ma
 TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
 fold.ma coq.ma
+ng_pts.ma 
 TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
@@ -130,7 +131,7 @@ TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
 TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
-ng_elim.ma 
+ng_elim.ma ng_pts.ma
 TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
@@ -157,7 +158,7 @@ TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
-ng_commands.ma nat/plus.ma
+ng_commands.ma nat/nat.ma ng_pts.ma
 TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
 paramodulation/BOO075-1.ma 
 TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
@@ -231,6 +232,7 @@ TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-4.p.ma logic/equality.ma
 TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
+lara.ma nat/nat.ma
 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
 paramodulation.ma coq.ma
 TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
@@ -334,6 +336,7 @@ TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
 coercions_open.ma logic/equality.ma nat/nat.ma
 paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
+ng_uris_and_notation.ma nat/nat.ma
 TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
 TPTP/Veloci/LAT008-1.p.ma logic/equality.ma