+let add_coercion f t (i, uri, vs) =
+ let rec add f x = match x with
+ | B.Sort _
+ | B.LRef _
+ | B.GRef _ -> f x
+ | B.Cast (u, t) ->
+ let f uu =
+ let f tt = f (S.sh2 u uu t tt x B.cast) in
+ add f t
+ in
+ add f u
+ | B.Appl (v, t) ->
+ let f vv =
+ let f tt = f (S.sh2 v vv t tt x B.appl) in
+ add f t
+ in
+ add f v
+ | B.Bind (l, _, _, _) when i = l ->
+ if U.eq uri I.imp then f (mk_gref I.mt (vs @ [x])) else
+ if U.eq uri I.all then f (mk_gref I.alli (vs @ [x])) else
+ assert false
+ | B.Bind (l, id, B.Abst w, t) ->
+ let f ww =
+ let f tt = f (S.sh2 w ww t tt x (B.bind_abst l id)) in
+ add f t
+ in
+ add f w
+ | B.Bind (l, id, B.Abbr v, t) ->
+ let f vv =
+ let f tt = f (S.sh2 v vv t tt x (B.bind_abbr l id)) in
+ add f t
+ in
+ add f v
+ | B.Bind (l, id, B.Void, t) ->
+ let f tt = f (S.sh1 t tt x (B.bind l id B.Void)) in
+ add f t
+ in
+ add f t
+
+let add_coercions f = C.list_fold_left f add_coercion
+