+let proj_fix (s, _, w, _) = s, w
+
+let proj_cofix (s, w, _) = s, w
+
+let mk_context proj discharge_term s =
+ let map e =
+ let s, w = proj e in
+ let w' = discharge_term w in
+ Some (C.Name s, C.Decl w')
+ in
+ List.length s, List.rev_map map s
+
+let rec split_absts named no c = function
+ | C.Lambda (s, w, t) ->
+ let e = Some (s, C.Decl w) in
+ let named = named && s <> C.Anonymous in
+ split_absts named (succ no) (e :: c) t
+ | t ->
+ named, no, c, t
+
+let close is_type c t =
+ let map t = function
+ | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
+ | Some (b, C.Decl w) ->
+ if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
+ | None -> assert false
+ in
+ List.fold_left map t c
+
+let relocate to_what from_what k m =
+ try
+ let u = List.nth from_what (m - k) in
+ let map v m = if UM.eq u v then Some m else None in
+ match X.list_findopt map to_what with
+ | Some m -> m + k
+ | None -> raise (Failure "nth")
+ with
+ | Failure "nth" -> assert false
+