- critical bug fixed in NCicSubstitution.lift:

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

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 =