X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fgrammar%2Flenv.ma;h=ba94738a85847b3a9327fd17d492797210605299;hb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;hp=5aacaf57ccaffe8127fa33a21982074ffe9fb681;hpb=eb918fc784eacd2094e3986ba321ef47690d9983;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
index 5aacaf57c..ba94738a8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term.ma".
+include "basic_2/grammar/term.ma".
 
 (* LOCAL ENVIRONMENTS *******************************************************)
 
@@ -36,3 +36,5 @@ interpretation "abbreviation (local environment)"
 
 interpretation "abstraction (local environment)"
    'DxAbst L T = (LPair L Abst T).
+
+(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)