diff options
| author | Hugo Herbelin | 2014-06-27 21:37:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-28 18:52:55 +0200 |
| commit | 1f0e44c96872196d0051618de77c4735eb447540 (patch) | |
| tree | 8b69aa789ebff430d021af431ad9ad453883ba25 /tactics | |
| parent | efa921c807e48cfc19943d2bfd7f4eb11f8f9e09 (diff) | |
Moved code for finding subterms (pattern, induction, set, generalize, ...)
into a specific new cleaned file find_subterm.ml.
This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
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' |