update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / genv.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
index 085e35dac7d0e8b484c8f5a9bf0cc79ea792d973..3e899a82986846d577da2853611171c5fb3923a4 100644 (file)
--- 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 *********************************************************)