]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralConversion.ml
Procedural: we corrected two errors about the handling of mutcase (the "cases"
[helm.git] / helm / software / components / acic_procedural / proceduralConversion.ml
index 3eadc2fcf985395f9613a64a859decb0fb45d515..97e32b94a458f1cdd3ce9bf9c49f30a21c5c675a 100644 (file)
@@ -59,7 +59,10 @@ let lift k n =
       | C.ARel (id, rid, m, b) as t -> 
          if m < k then t else 
         if m + n > 0 then C.ARel (id, rid, m + n, b) else
-        assert false
+        begin 
+           HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n);
+           assert false
+        end
       | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
       | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
       | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)