From 2e3ae20fe1ed3d7238286720c302bc892505caae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 18 Nov 2014 10:18:00 +0100
Subject: Fixing a little bug with nested but convertible occurrences in
 "destruct at".

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

(limited to 'pretyping')

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 30233cdf9e..28e52856c6 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -110,7 +110,13 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
     try
       let subst = test.match_fun test.testing_state t in
       if Locusops.is_selected !pos occs then
-        (add_subst t subst; incr pos;
+        (if !nested then begin
+          (* in case it is nested but not later detected as unconvertible,
+             as when matching "id _" in "id (id 0)" *)
+          let lastpos = Option.get test.last_found in
+          raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,None))
+         end;
+         add_subst t subst; incr pos;
          (* Check nested matching subterms *)
          nested := true; ignore (subst_below k t); nested := false;
          (* Do the effective substitution *)
-- 
cgit v1.2.3