diff options
| author | Hugo Herbelin | 2014-08-19 17:57:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-25 12:11:10 +0200 |
| commit | 19a7a5789c42a143f92232ce15298c2f44db96ba (patch) | |
| tree | 84f883a8a1834f7b031100822f64f6aaa15afee1 /test-suite | |
| parent | 965be8e6c441214542947b75e1625bc9068c40c9 (diff) | |
Fixing a bug introduced in the extension of 'apply in' + simplifying code.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/apply.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 57b030fc5d..1393843ece 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -446,3 +446,19 @@ Goal forall H:0=0, H = H. intros. Fail apply eq_sym in H. Abort. + +(* Check naming pattern in apply in *) + +Goal ((False /\ (True -> True))) -> True -> True. +intros F H. +apply F in H as H0. (* Check that H0 is not used internally *) +exact H0. +Qed. + +Goal ((False /\ (True -> True/\True))) -> True -> True/\True. +intros F H. +apply F in H as (?,?). +split. +exact H. (* Check that generated names are H and H0 *) +exact H0. +Qed. |