Use seed to avoid further name clashes.

[helm.git] / helm / software / components / cic / cicInspect.ml

diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml
index a1e94e247649f4fd6e5cd3237d3f15a4fd918fa3..cc911df84ac902fe9ae43b2284d1eca430a499ad 100644 (file)
--- a/helm/software/components/cic/cicInspect.ml
+++ b/helm/software/components/cic/cicInspect.ml
@@ -56,9 +56,10 @@ let get_rels_from_premise h t =
         in
         List.fold_left map g ss
       | C.Cast (t1, t2)    -> aux d (aux d g t2) t1
-      | C.LetIn (_, t1, t2)
       | C.Lambda (_, t1, t2)
       | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+      | C.LetIn (_, t1, ty, t2) ->
+         aux d (aux d (aux (succ d) g t2) ty) t1
       | C.MutCase (_, _, t1, t2, ss) ->
         aux d (aux d (List.fold_left (aux d) g ss) t2) t1
       | C.Fix (_, ss) ->
@@ -95,9 +96,9 @@ let get_mutinds_of_uri u t =
         in
         List.fold_left map g ss
       | C.Cast (t1, t2)              -> aux (aux g t2) t1
-      | C.LetIn (_, t1, t2)
       | C.Lambda (_, t1, t2)
-      | C.Prod (_, t1, t2)           -> aux (aux g t2) t1
+      | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux g t2) ty) t1
       | C.MutCase (_, _, t1, t2, ss) ->
         aux (aux (List.fold_left aux g ss) t2) t1
       | C.Fix (_, ss)                ->
@@ -128,9 +129,9 @@ let rec aux n = function
       in
       List.fold_left map (succ n) ss
    | C.Cast (t1, t2)
-   | C.LetIn (_, t1, t2)
    | C.Lambda (_, t1, t2)
-   | C.Prod (_, t1, t2)           -> aux (aux (succ n) t2) t1
+   | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
+   | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1
    | C.MutCase (_, _, t1, t2, ss) ->
       aux (aux (List.fold_left aux (succ n) ss) t2) t1
    | C.Fix (_, ss)                ->