diff options
author | 2015-10-19 18:18:34 +0200 | |
---|---|---|
committer | 2015-10-19 18:18:34 +0200 | |
commit | c7dcb76ffff6b12b031e906b002b4d76c1aaea50 (patch) | |
tree | 8d5115258c3b7042767e45d742e2800dab209822 /test-suite/success | |
parent | 666568377cbe1c18ce479d32f6359aa61af6d553 (diff) | |
parent | 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/ltac.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 6c4d4ae98..5bef2e512 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,29 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* Check that matching "match" does not look into the invisible + canonically generated binders of the return clause and of the branches *) + +Goal forall n, match n with 0 => true | S _ => false end = true. +intros. unfold nat_rect. +Fail match goal with |- context [nat] => idtac end. +Abort. + +(* Check that branches of automatically generated elimination + principle are correctly eta-expanded and hence matchable as seen + from the user point of view *) + +Goal forall a f n, nat_rect (fun _ => nat) a f n = 0. +intros. unfold nat_rect. +match goal with |- context [f _] => idtac end. +Abort. + +(* Check that branches of automatically generated elimination + principle are in correct form also in the presence of let-ins *) + +Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a. +Goal forall x, match x with c => 0 end = 1. +intros. +match goal with |- context [0] => idtac end. +Abort. |