AMBDA-TYPES: some improvements. subst now fully exploited

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma
index 844b19c34c85026b803185c084adc7a95d0856a5..f5c63fd0b78a4d329d58e10de16df799dd528d8d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma
@@ -21,7 +21,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Context".
 
 include "datatypes/Term.ma".
 
-inductive Context: Set \def
+inductive Context: Type \def
    | leaf: Context
    | intb: Context \to IntB \to Term \to Context
 .