new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[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 d62b6fec366ed110af0a82f1b5ef9c7e205b192b..4467f332ccd99e48c1c92a93eb1f8dc432824cd6 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -46,6 +46,7 @@ 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)