X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Flebesgue.ma;h=1b3f5025de55d3b50b8fed85c1f37f793c0db69c;hb=5755ebe4016316a474ad8ab8d33b1a1a9187cc9e;hp=f81c5ce46e452a2082062df61f48044f9c5ca870;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git

diff --git a/helm/software/matita/library/dama/lebesgue.ma b/helm/software/matita/library/dama/lebesgue.ma
index f81c5ce46..1b3f5025d 100644
--- a/helm/software/matita/library/dama/lebesgue.ma
+++ b/helm/software/matita/library/dama/lebesgue.ma
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* manca un pezzo del pullback, se inverto poi non tipa *)
-include "sandwich.ma".
-include "property_exhaustivity.ma".
+include "dama/sandwich.ma".
+include "dama/property_exhaustivity.ma".
 
 (* NOT DUALIZED *)
 alias symbol "low" = "lower".