X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fgenv.ma;h=3e899a82986846d577da2853611171c5fb3923a4;hp=085e35dac7d0e8b484c8f5a9bf0cc79ea792d973;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hpb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
index 085e35dac..3e899a829 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
@@ -23,20 +23,20 @@ include "basic_2/syntax/term.ma".
 (* global environments *)
 inductive genv: Type[0] ≝
 | GAtom: genv                       (* empty *)
-| GBind: genv → bind2 → term → genv (* binding construction *)
+| GPair: genv → bind2 → term → genv (* binary binding construction *)
 .
 
 interpretation "sort (global environment)"
    'Star = (GAtom).
 
 interpretation "global environment binding construction (binary)"
-   'DxBind2 G I T = (GBind G I T).
+   'DxBind2 G I T = (GPair G I T).
 
 interpretation "abbreviation (global environment)"
-   'DxAbbr G T = (GBind G Abbr T).
+   'DxAbbr G T = (GPair G Abbr T).
 
 interpretation "abstraction (global environment)"
-   'DxAbst G T = (GBind G Abst T).
+   'DxAbst G T = (GPair G Abst T).
 
 (* Basic properties *********************************************************)