X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Falpha_1%2Fsyntax%2Fterm.ma;h=4334a09188fdc805314f2bcec4f1e1e944c64250;hp=4ba35edc6f5518fbb76a0d7ef52f03899dfd6ab3;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
index 4ba35edc6..4334a0918 100644
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
+++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
@@ -47,13 +47,13 @@ interpretation "term construction (binary)"
    'SnItem2 I T1 T2 = (TPair I T1 T2).
 
 interpretation "character (term)"
-   'SnStar k T = (TUnit (Char k) T).
+   'SnStar s T = (TUnit (Char s) T).
 
 interpretation "local reference (term)"
    'SnLRef i T = (TUnit (LRef i) T).
 
 interpretation "global reference (term)"
-   'SnGRef p T = (TUnit (GRef p) T).
+   'SnGRef l T = (TUnit (GRef l) T).
 
 interpretation "negative abbreviation (term)"
    'SnAbbrNeg T = (TUnit Decl T).
@@ -62,7 +62,7 @@ interpretation "positive abstraction (term)"
    'SnAbstPos T1 T2 = (TPair Abst T1 T2).
 
 interpretation "abbreviation (term)"
-   'SnAbbr a T1 T2 = (TPair (Abbr a) T1 T2).
+   'SnAbbr p T1 T2 = (TPair (Abbr p) T1 T2).
 
 interpretation "positive abbreviation (term)"
    'SnAbbrPos T1 T2 = (TPair (Abbr true) T1 T2).
@@ -71,7 +71,7 @@ interpretation "negative abbreviation (term)"
    'SnAbbrNeg T1 T2 = (TPair (Abbr false) T1 T2).
 
 interpretation "projection (term)"
-   'SnProj a T1 T2 = (TPair (Proj a) T1 T2).
+   'SnProj p T1 T2 = (TPair (Proj p) T1 T2).
 
 interpretation "positive projection (term)"
    'SnProjPos T1 T2 = (TPair (Proj true) T1 T2).