- 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 32fa33ac845b5a272bf233f3644082d61a33245a..43a2f8174a74a1cad4696523908e8a4575f6933e 100644 (file)
--- 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 4198eae5fe37bd638cfabf32df2fb7decd36c7b5..ed14180aa670c7f41c6f8f28706ef53db6b4b419 100644 (file)
--- 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 =