From 8134330933e377a344b5ee38890198dc0b653428 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Oct 2009 16:52:01 +0000 Subject: [PATCH] Works again --- .../matita/contribs/ng_assembly/compiler/environment.ma | 2 -- 1 file changed, 2 deletions(-) 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; -- 2.39.2