From 51c8b16816ad0e9bdfaab0314fa6a0db5f4528f5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Nov 2014 15:46:13 +0100
Subject: Continuing fixing nested but convertible occurrences in find_subterm
 (see 2e3ae20fe1e): test was only relevant in the case of explicitly given
 occurrence numbers.

---
 pretyping/find_subterm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 28e52856c6..4a48a9b275 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
-- 
cgit v1.2.3