diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-19 15:46:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-19 18:48:34 +0100 |
| commit | 51c8b16816ad0e9bdfaab0314fa6a0db5f4528f5 (patch) | |
| tree | c1384a1cfce28eaf9af36858a5bc430494004caa /pretyping/find_subterm.ml | |
| parent | bc69260e1427d77e5a3faf2f14e4bc9b3acb354f (diff) | |
Continuing fixing nested but convertible occurrences in find_subterm
(see 2e3ae20fe1e): test was only relevant in the case of explicitly
given occurrence numbers.
Diffstat (limited to 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 28e52856c..4a48a9b27 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -118,7 +118,8 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t = end; add_subst t subst; incr pos; (* Check nested matching subterms *) - nested := true; ignore (subst_below k t); nested := false; + if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then + begin nested := true; ignore (subst_below k t); nested := false end; (* Do the effective substitution *) Vars.lift k (bywhat ())) else |