From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 10 May 2009 10:51:06 +0000 (+0000)
Subject: - critical bug fixed in NCicSubstitution.lift:
X-Git-Tag: make_still_working~3999
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a41b13ed498128bb99eb7cafa74ebbe10998c72c;p=helm.git

- 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.
---

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 =