milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 5b83675b3a62e855e74d9699b9c3ec58a2e13d28..66ddc0d99cedabd61df19e96ec724ff12ba811a4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -26,10 +26,10 @@ interpretation "native type assignment (term)"
    'Colon a h G L T U = (nta a h G L T U).
 
 interpretation "restricted native type assignment (term)"
-   'Colon h G L T U = (nta true h G L T U).
+   'Colon h G L T U = (nta (yinj (S (S O))) h G L T U).
 
 interpretation "extended native type assignment (term)"
-   'ColonStar h G L T U = (nta false h G L T U).
+   'ColonStar h G L T U = (nta Y h G L T U).
 
 (* Basic properties *********************************************************)