X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fgrammar%2Fterm.ma;h=3b6614361654328f5548874c8edc738713f32fbb;hb=37d40349c3c82a62a8cbced18545bfd526ebe7ff;hp=309df0b3f6b2e910977456c4cb521184d93afaac;hpb=b264ad188cb0023a16dae105b037357fa75c5c1a;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma
index 309df0b3f..3b6614361 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma
@@ -18,14 +18,15 @@ include "Basic-2/grammar/item.ma".
 
 (* terms *)
 inductive term: Type[0] ≝
-| TSort: nat → term                 (* sort: starting at 0 *)
-| TLRef: nat → term                 (* reference by index: starting at 0 *)
-| TPair: item2 → term → term → term (* binary item construction *)
+  | TAtom: item0 → term               (* atomic item construction *)
+  | TPair: item2 → term → term → term (* binary item construction *)
 .
 
-interpretation "sort (term)" 'Star k = (TSort k).
+interpretation "sort (term)" 'Star k = (TAtom (Sort k)).
 
-interpretation "local reference (term)" 'LRef i = (TLRef i).
+interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)).
+
+interpretation "term construction (atomic)" 'SItem I = (TAtom I).
 
 interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).