diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-25 07:49:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-25 07:49:24 +0000 |
| commit | 6e50e71e8ab3e501ec22b6d49cece3f6464e38d2 (patch) | |
| tree | 78bc9fd828c65c19f12b27b76072653d5894beb2 /test-suite/success/unification.v | |
| parent | e4aca4173b55133d1dcf273eb3796036342524d3 (diff) | |
Redondance erronée dans les tests
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9533 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/unification.v')
| -rw-r--r-- | test-suite/success/unification.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 2d6dabf26..4ddaab710 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -62,7 +62,7 @@ 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, +Lemma l4 : (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. @@ -82,7 +82,7 @@ Qed. This used to fail before revision 9389 in trunk *) -Lemma l4 : +Lemma l5 : forall f : (forall P, P true), (forall P, f P = f P) -> forall Q, f (fun x => Q x) = f (fun x => Q x). Proof. |