Fixing a little bug with nested but convertible occurrences in "destruct at".

3 files changed, 24 insertions, 10 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 30233cdf9..28e52856c 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 *)
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 56cdf18e6..277e3ca60 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -113,6 +113,12 @@ destruct (_, S _). (* Was unifying at some time in trunk, now takes the first oc
 change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n0).
 Abort.
 
+(* An example with incompatible but convertible occurrences *)
+
+Goal id (id 0) = 0.
+Fail destruct (id _) at 1 2.
+Abort.
+
 (* Avoid unnatural selection of a subterm larger than expected *)
 
 Goal let g := fun x:nat => x in g (S 0) = 0.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4ca22640d..44e98a513 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -680,15 +680,17 @@ let pr_position (cl,pos) =
   int pos ++ clpos
 
 let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) e =
-  let s = if nested then "Found nested occurrences of the pattern"
-    else "Found incompatible occurrences of the pattern" in
-  let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in
-  str s ++ str ":" ++
-  spc () ++ str "Matched term " ++ pr_lconstr_env env sigma t2 ++
-  strbrk " at position " ++ pr_position (cl2,pos2) ++
-  strbrk " is not compatible with matched term " ++
-  pr_lconstr_env env sigma t1 ++ strbrk " at position " ++
-  pr_position (cl1,pos1) ++ ppreason ++ str "."
+  if nested then
+    str "Found nested occurrences of the pattern at positions " ++
+    int pos1 ++ strbrk " and " ++ pr_position (cl2,pos2) ++ str "."
+  else
+    let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in
+    str "Found incompatible occurrences of the pattern" ++ str ":" ++
+    spc () ++ str "Matched term " ++ pr_lconstr_env env sigma t2 ++
+    strbrk " at position " ++ pr_position (cl2,pos2) ++
+    strbrk " is not compatible with matched term " ++
+    pr_lconstr_env env sigma t1 ++ strbrk " at position " ++
+    pr_position (cl1,pos1) ++ ppreason ++ str "."
 
 let pr_constraints printenv env sigma evars cstrs =
   let (ev, evi) = Evar.Map.choose evars in