diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 |
2 files changed, 4 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6adec45bc9..fa2ac37126 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -582,7 +582,7 @@ END (**********************************************************************) let subst_var_with_hole occ tid t = - let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in + let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function | GVar (_,id) as x -> @@ -598,7 +598,7 @@ let subst_var_with_hole occ tid t = | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t in - if !occref > 0 then Termops.error_invalid_occurrence [occ] else t' + if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' let subst_hole_with_term occ tc t = let locref = ref 0 in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 30568edab4..d046a06427 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,6 +15,7 @@ open Term open Vars open Context open Termops +open Find_subterm open Namegen open Declarations open Inductiveops @@ -1865,7 +1866,7 @@ let generalize_goal_gen ids i ((occs,c,b),na) t (cl,evd) = let decls,cl = decompose_prod_n_assum i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in - let cl',evd' = subst_closed_term_univs_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in + let cl',evd' = subst_closed_term_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name c t ids cl' na in mkProd_or_LetIn (na,b,t) cl', evd' |