match concl_pat with
None -> Cic.Implicit (Some `Hole)
| Some path -> path in
- let roots = CicUtil.select ~term:ty ~context:path in
+ let roots = ProofEngineHelpers.select ~term:ty ~pattern:path in
List.fold_left
(fun acc (i, r) ->
ProofEngineHelpers.find_subterms