X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta.ma;h=e51a43fdc8989569f6212f4a99e92912f7168d48;hb=bac74b5cff042d37e1abc9c961a6c41094b8a294;hp=187370fab65a16de7c9c9d0c489a272a3733f56e;hpb=cacd7323994f7621286dbfd93bbf4c50acfbe918;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 187370fab..e51a43fdc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -20,16 +20,16 @@ include "basic_2/dynamic/cnv.ma".
 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
 
 definition nta (a) (h): relation4 genv lenv term term ≝
-                        λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
+           λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
 
 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 (yinj (S (S O))) h G L T U).
+   'Colon h G L T U = (nta (ac_eq (S O)) h G L T U).
 
 interpretation "extended native type assignment (term)"
-   'ColonStar h G L T U = (nta Y h G L T U).
+   'ColonStar h G L T U = (nta ac_top h G L T U).
 
 (* Basic properties *********************************************************)