Fixing an unnatural selection of subterms larger than expected in the

presence of let-ins.

2 files changed, 11 insertions, 1 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 29ed69b2dd..29d721577f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1526,7 +1526,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
 
 let secondOrderAbstraction env evd flags typ (p, oplist) =
   (* Remove delta when looking for a subterm *)
-  let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
+  let flags = { flags with modulo_delta = empty_transparent_state } in
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 4a7657e292..48927b6cc3 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -110,3 +110,13 @@ Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
 do 2 eexists.
 Fail destruct (_, S _). (* Was succeeding at some time in trunk *)
 Show Proof.
+
+(* Avoid unnatural selection of a subterm larger than expected *)
+
+Goal let g := fun x:nat => x in g (S 0) = 0.
+intro.
+destruct S.
+(* Check that it is not the larger subterm "f (S 0)" which is
+   selected, as it was the case in 8.4 *)
+unfold g at 1.
+Abort.