X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FUnified-Sub%2FContext%2Fdefs.ma;h=4da3c95d70ea568a7df0270ffc31f30748f40f20;hb=ac7831c825d6c3227053f3e339a53b10e3e7118f;hp=7aca13a59213ca2b238bc9d8afa8697f98d94e34;hpb=8f5b25b6091f1e240f37de5355e7a99b756e98e8;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
index 7aca13a59..4da3c95d7 100644
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
@@ -23,5 +23,5 @@ include "Term/defs.ma".
 
 inductive Context: Set \def
    | leaf: Context
-   | head: Context \to Bind \to Term \to Context
+   | intb: Context \to IntB \to Term \to Context
 .