diff options
| -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 |