-let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
- terms ~status:((proof,goal) as status)
-=
- let module C = Cic in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let typ =
- match terms with
- [] -> assert false
- | he::tl ->
- (* We need to check that all the convertibility of all the terms *)
- List.iter
- (function t ->
- if not (CicReduction.are_convertible context he t) then
- raise AllSelectedTermsMustBeConvertible
- ) tl ;
- (CicTypeChecker.type_of_aux' metasenv context he)
+let generalize_tac
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ ~term pattern
+ =
+ let module PET = ProofEngineTypes in
+ let generalize_tac mk_fresh_name_callback ~term (hyps_pat,concl_pat) status =
+ if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ;
+ let (proof, goal) = status in
+ let module C = Cic in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let _,metasenv,_,_ = proof in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let terms =
+ let path =
+ match concl_pat with
+ None -> Cic.Implicit (Some `Hole)
+ | Some path -> path in
+ let roots = ProofEngineHelpers.select ~term:ty ~pattern:path in
+ List.fold_left
+ (fun acc (i, r) ->
+ ProofEngineHelpers.find_subterms
+ ~eq:ProofEngineReduction.alpha_equivalence ~wanted:term r @ acc
+ ) [] roots