diff options
Diffstat (limited to 'test-suite/success')
26 files changed, 90 insertions, 57 deletions
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index 69dc9aca78..d52a853aae 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,4 +1,4 @@ -(* Cf coqbugs #546 *) +(* Cf BZ#546 *) Require Import Omega. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 06f807f29a..893d75b77f 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -64,7 +64,7 @@ Check (fun x:I1 => end). (* Check implicit parameters of inductive types (submitted by Pierre - Casteran and also implicit in #338) *) + Casteran and also implicit in BZ#338) *) Set Implicit Arguments. Unset Strict Implicit. @@ -80,7 +80,7 @@ Inductive Finite (A : Set) : LList A -> Prop := | Finite_LCons : forall (a : A) (l : LList A), Finite l -> Finite (LCons a l). -(* Check positivity modulo reduction (cf bug #983) *) +(* Check positivity modulo reduction (cf bug BZ#983) *) Record P:Type := {PA:Set; PB:Set}. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 850f094348..45c71615fc 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -1,6 +1,6 @@ Axiom magic : False. -(* Submitted by Dachuan Yu (bug #220) *) +(* Submitted by Dachuan Yu (BZ#220) *) Fixpoint T (n : nat) : Type := match n with | O => nat -> Prop @@ -16,7 +16,7 @@ Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l. inversion 1. Abort. -(* Submitted by Pierre Casteran (bug #540) *) +(* Submitted by Pierre Casteran (BZ#540) *) Set Implicit Arguments. Unset Strict Implicit. @@ -64,7 +64,7 @@ elim magic. elim magic. Qed. -(* Submitted by Boris Yakobowski (bug #529) *) +(* Submitted by Boris Yakobowski (BZ#529) *) (* Check that Inversion does not fail due to unnormalized evars *) Set Implicit Arguments. @@ -100,7 +100,7 @@ intros a b H. inversion H. Abort. -(* Check non-regression of bug #1968 *) +(* Check non-regression of BZ#1968 *) Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t). Goal forall o, foo2 o -> 0 = 1. @@ -130,7 +130,7 @@ Proof. intros. inversion H. Abort. -(* Bug #2314 (simplified): check that errors do not show as anomalies *) +(* BZ#2314 (simplified): check that errors do not show as anomalies *) Goal True -> True. intro. @@ -158,7 +158,7 @@ reflexivity. Qed. (* Up to September 2014, Mapp below was called MApp0 because of a bug - in intro_replacing (short version of bug 2164.v) + in intro_replacing (short version of BZ#2164.v) (example taken from CoLoR) *) Parameter Term : Type. diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v index d5e1a38cf5..6c59bf6edb 100644 --- a/test-suite/success/Mod_type.v +++ b/test-suite/success/Mod_type.v @@ -1,4 +1,4 @@ -(* Check bug #1025 submitted by Pierre-Luc Carmel Biron *) +(* Check BZ#1025 submitted by Pierre-Luc Carmel Biron *) Module Type FOO. Parameter A : Type. @@ -18,7 +18,7 @@ Module Bar : BAR. End Bar. -(* Check bug #2809: correct printing of modules with notations *) +(* Check BZ#2809: correct printing of modules with notations *) Module C. Inductive test : Type := diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 4d04f2cf9b..e3f90f6d94 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -1,5 +1,5 @@ (* Check that "where" clause behaves as if given independently of the *) -(* definition (variant of bug #1132 submitted by Assia Mahboubi) *) +(* definition (variant of BZ#1132 submitted by Assia Mahboubi) *) Fixpoint plus1 (n m:nat) {struct n} : nat := match n with diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index ecbf04e412..470e4f0580 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z. Qed. End B. -(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *) Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. @@ -86,7 +86,7 @@ intros; omega. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) -(* Submitted by Hubert Thierry (bug #743) *) +(* Submitted by Hubert Thierry (BZ#743) *) (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index b8f8660e9c..6fd936935c 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -132,7 +132,7 @@ intros. omega. Qed. -(* Magaud #240 *) +(* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros. diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v index c4d086a348..4e726335c9 100644 --- a/test-suite/success/Omega2.v +++ b/test-suite/success/Omega2.v @@ -1,6 +1,6 @@ Require Import ZArith Omega. -(* Submitted by Yegor Bryukhov (#922) *) +(* Submitted by Yegor Bryukhov (BZ#922) *) Open Scope Z_scope. diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 801ece9e3d..0df3d5685d 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z. Qed. End B. -(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *) Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. @@ -88,7 +88,7 @@ romega with nat. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) -(* Submitted by Hubert Thierry (bug #743) *) +(* Submitted by Hubert Thierry (BZ#743) *) (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m : nat, le n (plus n (mult n m)). Proof. diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 42730f2e16..3ddf6a40fb 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -132,7 +132,7 @@ intros. romega. Qed. -(* Magaud #240 *) +(* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. @@ -146,7 +146,7 @@ intros x y. romega. Qed. -(* Besson #1298 *) +(* Besson BZ#1298 *) Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. Proof. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 87e8c8e33e..43eda67ea3 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -1,6 +1,6 @@ Require Import ZArith ROmega. -(* Submitted by Yegor Bryukhov (#922) *) +(* Submitted by Yegor Bryukhov (BZ#922) *) Open Scope Z_scope. diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v new file mode 100644 index 0000000000..58ae5b8fb8 --- /dev/null +++ b/test-suite/success/ROmega4.v @@ -0,0 +1,26 @@ +(** ROmega is now aware of the bodies of context variables + (of type Z or nat). + See also #148 for the corresponding improvement in Omega. +*) + +Require Import ZArith ROmega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +romega. +Qed. + +(** Example seen in #4132 + (actually solvable even if b isn't known to be 5) *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +romega. +Qed. diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v index 0576f3c68f..2789c6c9a6 100644 --- a/test-suite/success/Rename.v +++ b/test-suite/success/Rename.v @@ -4,7 +4,7 @@ rename n into p. induction p; auto. Qed. -(* Submitted by Iris Loeb (#842) *) +(* Submitted by Iris Loeb (BZ#842) *) Section rename. diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v index 361c787e25..76aac39a55 100644 --- a/test-suite/success/Try.v +++ b/test-suite/success/Try.v @@ -1,5 +1,5 @@ (* To shorten interactive scripts, it is better that Try catches - non-existent names in Unfold [cf bug #263] *) + non-existent names in Unfold [cf BZ#263] *) Lemma lem1 : True. try unfold i_dont_exist. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 90a60daa66..0219c3bfdf 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -12,7 +12,7 @@ assumption. assumption. Qed. -(* Simplification of bug 711 *) +(* Simplification of BZ#711 *) Parameter f : true = false. Goal let p := f in True. @@ -37,7 +37,7 @@ Goal True. case Refl || ecase Refl. Abort. -(* Submitted by B. Baydemir (bug #1882) *) +(* Submitted by B. Baydemir (BZ#1882) *) Require Import List. @@ -385,7 +385,7 @@ intros. Fail destruct H. Abort. -(* Check keep option (bug #3791) *) +(* Check keep option (BZ#3791) *) Goal forall b:bool, True. intro b. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index c36313ec16..627794832d 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -23,7 +23,7 @@ Definition f1 frm0 a1 : B := f frm0 a1. (* Checks that solvable ? in the type part of the definition are harmless *) Definition f2 frm0 a1 : B := f frm0 a1. -(* Checks that sorts that are evars are handled correctly (bug 705) *) +(* Checks that sorts that are evars are handled correctly (BZ#705) *) Require Import List. Fixpoint build (nl : list nat) : @@ -58,7 +58,7 @@ Check (forall y n : nat, {q : nat | y = q * n}) -> forall n : nat, {q : nat | x = q * n}). -(* Check instantiation of nested evars (bug #1089) *) +(* Check instantiation of nested evars (BZ#1089) *) Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). @@ -188,7 +188,7 @@ Abort. End Additions_while. -(* Two examples from G. Melquiond (bugs #1878 and #1884) *) +(* Two examples from G. Melquiond (BZ#1878 and BZ#1884) *) Parameter F1 G1 : nat -> Prop. Goal forall x : nat, F1 x -> G1 x. @@ -207,7 +207,7 @@ Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := | (existT _ k v)::l' => (existT _ k v):: (filter A l') end. -(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by +(* BZ#2000: used to raise Out of memory in 8.2 while it should fail by lack of information on the conclusion of the type of j *) Goal True. @@ -381,7 +381,7 @@ Section evar_evar_occur. Check match g _ with conj a b => f _ a b end. End evar_evar_occur. -(* Eta expansion (bug #2936) *) +(* Eta expansion (BZ#2936) *) Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c diff --git a/test-suite/success/if.v b/test-suite/success/if.v index 9fde95e80d..c81d2b9bf1 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -3,7 +3,7 @@ Check (fun b : bool => if b then Type else nat). -(* Check correct use of if-then-else predicate annotation (cf bug 690) *) +(* Check correct use of if-then-else predicate annotation (cf BZ#690) *) Check fun b : bool => if b as b0 return (if b0 then b0 = true else b0 = false) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index ee69df9774..a329894aad 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -1,5 +1,5 @@ (* Thinning introduction hypothesis must be done after all introductions *) -(* Submitted by Guillaume Melquiond (bug #1000) *) +(* Submitted by Guillaume Melquiond (BZ#1000) *) Goal forall A, A -> True. intros _ _. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 29e373eaa5..0f22a1f0a0 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -147,7 +147,7 @@ check_binding ipattern:(H). Abort. (* Check that variables explicitly parsed as ltac variables are not - seen as intro pattern or constr (bug #984) *) + seen as intro pattern or constr (BZ#984) *) Ltac afi tac := intros; tac. Goal 1 = 2. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 352abb2af5..b8a8ff7561 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -31,7 +31,7 @@ Proof. end). Abort. -(* Submitted by Roland Zumkeller (bug #888) *) +(* Submitted by Roland Zumkeller (BZ#888) *) (* The Fix and CoFix rules expect a subgoal even for closed components of the (co-)fixpoint *) @@ -43,7 +43,7 @@ Goal nat -> nat. exact 0. Qed. -(* Submitted by Roland Zumkeller (bug #889) *) +(* Submitted by Roland Zumkeller (BZ#889) *) (* The types of metas were in metamap and they were not updated when passing through a binder *) @@ -56,7 +56,7 @@ Goal forall n : nat, nat -> n = 0. end). Abort. -(* Submitted by Roland Zumkeller (bug #931) *) +(* Submitted by Roland Zumkeller (BZ#931) *) (* Don't turn dependent evar into metas *) Goal (forall n : nat, n = 0 -> Prop) -> Prop. @@ -65,7 +65,7 @@ intro P. reflexivity. Abort. -(* Submitted by Jacek Chrzaszcz (bug #1102) *) +(* Submitted by Jacek Chrzaszcz (BZ#1102) *) (* le problème a été résolu ici par normalisation des evars présentes dans les types d'evars, mais le problème reste a priori ouvert dans diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 1f24ef2a6b..c8dfcd2cbf 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -33,7 +33,8 @@ Qed. Add Setoid set same setoid_set as setsetoid. -Add Morphism In : In_ext. +Add Morphism In with signature (eq ==> same ==> iff) as In_ext. +Proof. unfold same; intros a s t H; elim (H a); auto. Qed. @@ -50,10 +51,9 @@ simpl; right. apply (H2 H1). Qed. -Add Morphism Add : Add_ext. +Add Morphism Add with signature (eq ==> same ==> same) as Add_ext. split; apply add_aux. assumption. - rewrite H. reflexivity. Qed. @@ -90,7 +90,7 @@ Qed. Parameter P : set -> Prop. Parameter P_ext : forall s t : set, same s t -> P s -> P t. -Add Morphism P : P_extt. +Add Morphism P with signature (same ==> iff) as P_extt. intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption). Qed. @@ -113,7 +113,7 @@ Definition f: forall A : Set, A -> A := fun A x => x. Add Relation (id A) (rel A) as eq_rel. -Add Morphism (@f A) : f_morph. +Add Morphism (@f A) with signature (eq ==> eq) as f_morph. Proof. unfold rel, f. trivial. Qed. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 6baf79701a..79467e549c 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -134,8 +134,8 @@ Axiom SetoidS2 : Setoid_Theory S2 eqS2. Add Setoid S2 eqS2 SetoidS2 as S2setoid. Axiom f : S1 -> nat -> S2. -Add Morphism f : f_compat. Admitted. -Add Morphism f : f_compat2. Admitted. +Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat. Admitted. +Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat2. Admitted. Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). intros. @@ -151,7 +151,7 @@ Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). Qed. Axiom g : S1 -> S2 -> nat. -Add Morphism g : g_compat. Admitted. +Add Morphism g with signature (eqS1 ==> eqS2 ==> eq) as g_compat. Admitted. Axiom P : nat -> Prop. Theorem test2: @@ -190,13 +190,13 @@ Theorem test5: Qed. Axiom f_test6 : S2 -> Prop. -Add Morphism f_test6 : f_test6_compat. Admitted. +Add Morphism f_test6 with signature (eqS2 ==> iff) as f_test6_compat. Admitted. Axiom g_test6 : bool -> S2. -Add Morphism g_test6 : g_test6_compat. Admitted. +Add Morphism g_test6 with signature (eq ==> eqS2) as g_test6_compat. Admitted. Axiom h_test6 : S1 -> bool. -Add Morphism h_test6 : h_test6_compat. Admitted. +Add Morphism h_test6 with signature (eqS1 ==> eq) as h_test6_compat. Admitted. Theorem test6: forall E1 E2, (eqS1 E1 E2) -> (f_test6 (g_test6 (h_test6 E2))) -> @@ -223,7 +223,7 @@ Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. Instance eqS1_test8_default : DefaultRelation eqS1_test8. Axiom f_test8 : S2 -> S1_test8. -Add Morphism f_test8 : f_compat_test8. Admitted. +Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted. Axiom eqS1_test8': S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8' : Setoid_Theory S1_test8 eqS1_test8'. @@ -233,7 +233,7 @@ Add Setoid S1_test8 eqS1_test8' SetoidS1_test8' as S1_test8setoid'. (S1_test8, eqS1_test8'). However this does not happen and there is still no syntax for it ;-( *) Axiom g_test8 : S1_test8 -> S2. -Add Morphism g_test8 : g_compat_test8. Admitted. +Add Morphism g_test8 with signature (eqS1_test8 ==> eqS2) as g_compat_test8. Admitted. Theorem test8: forall x x': S2, (eqS2 x x') -> diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 5b87e877bf..1bfb8580b3 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. (* Check that inversion of names of mutual inductive fixpoints works *) -(* (cf bug #1031) *) +(* (cf BZ#1031) *) Inductive tree : Set := | node : nat -> forest -> tree diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 6f7498d659..1ffc026730 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -43,7 +43,7 @@ Check (fun _h1 => (zenon_notall nat _ (fun _T_0 => (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)). -(* Core of an example submitted by Ralph Matthes (#849) +(* Core of an example submitted by Ralph Matthes (BZ#849) It used to fail because of the K-variable x in the type of "sum_rec ..." which was not in the scope of the evar ?B. Solved by a head @@ -131,7 +131,7 @@ try case nonemptyT_intro. (* check that it fails w/o anomaly *) Abort. (* Test handling of return type and when it is decided to make the - predicate dependent or not - see "bug" #1851 *) + predicate dependent or not - see "bug" BZ#1851 *) Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True). intros. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index fc74225d76..2863404590 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -20,8 +20,7 @@ intro P; pattern P. apply lem2. Abort. -(* Check managing of universe constraints in inversion *) -(* Bug report #855 *) +(* Check managing of universe constraints in inversion (BZ#855) *) Inductive dep_eq : forall X : Type, X -> X -> Prop := | intro_eq : forall (X : Type) (f : X), dep_eq X f f @@ -40,7 +39,7 @@ Proof. Abort. -(* Submitted by Bas Spitters (bug report #935) *) +(* Submitted by Bas Spitters (BZ#935) *) (* This is a problem with the status of the type in LetIn: is it a user-provided one or an inferred one? At the current time, the diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v index 672222bdd6..a4fa544cd9 100644 --- a/test-suite/success/unshelve.v +++ b/test-suite/success/unshelve.v @@ -9,3 +9,11 @@ unshelve (refine (F _ _ _ _)). + exact (@eq_refl bool true). + exact (@eq_refl unit tt). Qed. + +(* This was failing in 8.6, because of ?a:nat being wrongly duplicated *) + +Goal (forall a : nat, a = 0 -> True) -> True. +intros F. +unshelve (eapply (F _);clear F). +2:reflexivity. +Qed. |