diff options
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 29ed69b2d..29d721577 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 4a7657e29..48927b6cc 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. |