Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / compiler / environment.ma

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