X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fenvironment.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fenvironment.ma;h=97183a6615f98b906f18e34eba576bbc1feac4e6;hb=8134330933e377a344b5ee38890198dc0b653428;hp=4467f332ccd99e48c1c92a93eb1f8dc432824cd6;hpb=08e552969f366bd18b5bb7515bbc514576a9b395;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 4467f332c..97183a661 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -46,8 +46,6 @@ 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));
- XXX nuova instantiate!
- (* 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)
  ##| ##2: #n; #dsc; #sub; #H;