+
+let get_clears c p xet =
+ let meta = C.Implicit None in
+ let rec aux c names p et = function
+ | [] ->
+ List.rev c, List.rev names
+ | Some (C.Name name as n, C.Decl v) as hd :: tl ->
+ let hd, names, v =
+ if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then
+ Some (C.Anonymous, C.Decl v), name :: names, meta
+ else
+ hd, names, v
+ in
+ let p = C.Lambda (n, v, p) in
+ let et = C.Prod (n, v, et) in
+ aux (hd :: c) names p et tl
+ | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
+ let hd, names, v =
+ if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then
+ Some (C.Anonymous, C.Def (v, x)), name :: names, meta
+ else
+ hd, names, v
+ in
+ let p = C.LetIn (n, v, p) in
+ let et = C.LetIn (n, v, et) in
+ aux (hd :: c) names p et tl
+ | Some (C.Anonymous as n, C.Decl v) as hd :: tl ->
+ let p = C.Lambda (n, meta, p) in
+ let et = C.Lambda (n, meta, et) in
+ aux (hd :: c) names p et tl
+ | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
+ let p = C.LetIn (n, meta, p) in
+ let et = C.LetIn (n, meta, et) in
+ aux (hd :: c) names p et tl
+ | None :: tl -> assert false
+ in
+ match xet with
+ | Some et -> aux [] [] p et c
+ | None -> c, []
+
+let clear c hyp =
+ let rec aux c = function
+ | [] -> List.rev c
+ | Some (C.Name name, entry) :: tail when name = hyp ->
+ aux (Some (C.Anonymous, entry) :: c) tail
+ | entry :: tail -> aux (entry :: c) tail
+ in
+ aux [] c