diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/unification.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 60c03831a0..6886962156 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -48,3 +48,18 @@ Parameter t: L (unit + unit). Check (f (fun x : unit + unit => sum_rec (fun _ : unit + unit => L unit) (fun y => c y) (fun y => c y) x) t). + + +(* Test patterns unification in apply *) + +Require Import Arith. +Parameter x y : nat. +Parameter G:x=y->x=y->Prop. +Parameter K:x<>y->x<>y->Prop. +Lemma l3 : (forall f:x=y->Prop, forall g:x<>y->Prop, + match eq_nat_dec x y with left a => f a | right a => g a end) + -> match eq_nat_dec x y with left a => G a a | right a => K a a end. +Proof. +intros. +apply H. +Qed. |