From a41b13ed498128bb99eb7cafa74ebbe10998c72c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 10 May 2009 10:51:06 +0000 Subject: [PATCH] - critical bug fixed in NCicSubstitution.lift: (0,Irl 0) was lifted to (1,Irl 0) but later on NCicTypechecker.check_metasenv_consistency assumes the invariant that the currenct context has length (m+n) if the metavariable is (m,Irl n). But this invariant is false in the case (m, Irl 0) when m > 0. - in NCicRefiner there was one line to normalize (m,Irl 0) and (m,Ctx []) to (0,...). Is it still required after the first patch to the kernel? I suspect no, thus I put an assert false to check. --- helm/software/components/ng_kernel/nCicSubstitution.ml | 1 + helm/software/components/ng_refiner/nCicRefiner.ml | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 32fa33ac8..43a2f8174 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -25,6 +25,7 @@ let debug_print = fun _ -> ();; let lift_from k n = let rec liftaux k = function | C.Rel m as t -> if m < k then t else C.Rel (m + n) + | C.Meta (i,(m,(C.Irl 0 as l))) when k <= m+1 -> C.Meta (i,(m,l)) | C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l)) | C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t | C.Meta (i,(m,l)) -> diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 4198eae5f..ed14180aa 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -384,8 +384,8 @@ and force_to_sort hdb match NCicReduction.whd ~subst context ty with | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> metasenv, subst, t, ty - | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> - metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) + | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ??? + metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *) | C.Meta (i,(_,lc)) -> let len = match lc with C.Irl len->len | C.Ctx l->List.length l in let metasenv, subst, newmeta = -- 2.39.2