LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Unified-Sub / datatypes / Term.ma

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 e1f090d1ad56dec5fa9c8775874f4b55cac77524..d1a98de5a03a70749e9c52df5eb41c1efd679ad9 100644 (file)
--- 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