X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fenvironment.ma;h=5b1408931c32144fbe758d1851189681f9a84f3a;hb=3e758134d629980e9bf018a913404b98eccc514c;hp=d62b6fec366ed110af0a82f1b5ef9c7e205b192b;hpb=c6ec0dc44c2e592c7b1323304052bc1a523e7c22;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index d62b6fec3..5b1408931 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -13,9 +13,10 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -46,9 +47,8 @@ ndefinition defined_envList ≝
 nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
  #d; #l;
  ngeneralize in match (refl_eq ? (S d));
- (* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
  ncases l in ⊢ (? ? % ? → %);
- ##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)
+ ##[ ##1: #dsc; #H; ndestruct (*nelim (nat_destruct_0_S … H)*)
  ##| ##2: #n; #dsc; #sub; #H;
           nnormalize;
           napply I