]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/variousTactics.ml
1) moved select and pattern_of from cicUtil to proofEngineHelpers
[helm.git] / helm / ocaml / tactics / variousTactics.ml
index 233cc321f4b5112006201d1609d294d59588274d..9fcbb966fc2d9ae3072df98935d31bbdb1059fd7 100644 (file)
@@ -88,7 +88,7 @@ let generalize_tac
       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