(function (i,_,_) ->
not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
;;
+
+(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
+let find_subterms ~eq ~wanted t =
+ let rec find wanted t =
+ if eq wanted t then
+ [t]
+ else
+ match t with
+ | Cic.Sort _
+ | Cic.Rel _ -> []
+ | Cic.Meta (_, ctx) ->
+ List.fold_left (
+ fun acc e ->
+ match e with
+ | None -> acc
+ | Some t -> find wanted t @ acc
+ ) [] ctx
+ | Cic.Lambda (_, t1, t2)
+ | Cic.Prod (_, t1, t2)
+ | Cic.LetIn (_, t1, t2) ->
+ find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2
+ | Cic.Appl l ->
+ List.fold_left (fun acc t -> find wanted t @ acc) [] l
+ | Cic.Cast (t, ty) -> find wanted t @ find wanted ty
+ | Cic.Implicit _ -> assert false
+ | Cic.Const (_, esubst)
+ | Cic.Var (_, esubst)
+ | Cic.MutInd (_, _, esubst)
+ | Cic.MutConstruct (_, _, _, esubst) ->
+ List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst
+ | Cic.MutCase (_, _, outty, indterm, patterns) ->
+ find wanted outty @ find wanted indterm @
+ List.fold_left (fun acc p -> find wanted p @ acc) [] patterns
+ | Cic.Fix (_, funl) ->
+ List.fold_left (
+ fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ ) [] funl
+ | Cic.CoFix (_, funl) ->
+ List.fold_left (
+ fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ ) [] funl
+ in
+ find wanted t