X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBase-2%2Fpreamble.ma;h=114efbd53479edff13a2103421c2283d46a30219;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=5bf2f44ef61b2e67060439408e2c106195174026;hpb=1a5e02c5d5048ee6ec7d207b77cd5c2c1bdb3dae;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
index 5bf2f44ef..114efbd53 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "Base-1/definitions.ma".
+include "Legacy-2/theory.ma".
 
 alias symbol "minus" = "Coq's natural minus".
 alias symbol "lt" = "Coq's natural 'less than'".