matitaGui: some missing cases during disambiguation now treated

[helm.git] / components / content_pres / proceduralConversion.ml

diff --git a/components/content_pres/proceduralConversion.ml b/components/content_pres/proceduralConversion.ml
index e506a8f6eec7581614291cfd1abbf71003def272..abd6fd62a8f897f7df4e2b884258706db50804bf 100644 (file)
--- a/components/content_pres/proceduralConversion.ml
+++ b/components/content_pres/proceduralConversion.ml
@@ -30,3 +30,32 @@ let rec need_whd i = function
    | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
    | _                    when i > 0 -> true
    | _                               -> false
+
+let lift k n =
+   let rec lift_xns k (uri, t) = uri, lift_term k t
+   and lift_ms k = function
+      | None   -> None
+      | Some t -> Some (lift_term k t)
+   and lift_fix len k (id, name, i, ty, bo) =
+      id, name, i, lift_term k ty, lift_term (k + len) bo
+   and lift_cofix len k (id, name, ty, bo) =
+      id, name, lift_term k ty, lift_term (k + len) bo
+   and lift_term k = function
+      | C.ASort _ as t -> t
+      | C.AImplicit _ as t -> t
+      | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b)
+      | 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)
+      | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
+      | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
+      | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
+      | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
+      | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
+      | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
+      | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
+      | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
+      | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
+      | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
+   in
+   lift_term k