X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Fgenv.ma;h=3308b79edf4a8d3bc4d1e8e307ba95c17531c5ef;hb=06d5ff2316426acfb16a9cc9784d40ce19351771;hp=38757ca1643dad295ab0d5a814fbe1eb56e2929f;hpb=29973426e0227ee48368d1c24dc0c17bf2baef77;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma index 38757ca16..3308b79ed 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma @@ -27,7 +27,7 @@ definition genv ≝ list2 bind2 term. interpretation "sort (global environment)" 'Star = (nil2 bind2 term). -interpretation "environment binding construction (binary)" +interpretation "global environment binding construction (binary)" 'DxBind2 L I T = (cons2 bind2 term I T L). interpretation "abbreviation (global environment)"