X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FUnified-Sub%2Fdatatypes%2FTerm.ma;h=d1a98de5a03a70749e9c52df5eb41c1efd679ad9;hb=e92710b1d9774a6491122668c8463b8658114610;hp=e1f090d1ad56dec5fa9c8775874f4b55cac77524;hpb=bd5488c8eaa88e27d6e9e6c46566f1ed8f1a59b0;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma
index e1f090d1a..d1a98de5a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 (* POLARIZED TERMS
    - Naming policy:
      - natural numbers      : sorts h k, local references i j, lengths l o
@@ -24,7 +22,7 @@
      - terms                : t u
 *)
 
-include "preamble4.ma".
+include "Unified-Sub/preamble.ma".
 
 inductive Bind: Type \def
    | abbr: Bind