contribs: some improvements

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Unified-Sub / Lift / defs.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
index 131d65133a09328bd6c2adae8f54d2164877b5c2..d8ee64fe5d0707dec483f9fbf657e91a4234836b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
    - Usage: invoke with positive polarity
 *)
 
-include "Term/defs.ma".
+include "datatypes/Term.ma".
 
 inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
    | lift_sort   : \forall i,h.