From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- test-suite/bench/lists-100.v | 2 +- test-suite/bench/lists_100.v | 2 +- test-suite/bugs/closed/shouldsucceed/1414.v | 4 +-- test-suite/bugs/closed/shouldsucceed/1784.v | 2 +- test-suite/bugs/closed/shouldsucceed/1844.v | 2 +- test-suite/bugs/closed/shouldsucceed/1935.v | 2 +- test-suite/bugs/closed/shouldsucceed/2127.v | 4 +-- test-suite/bugs/closed/shouldsucceed/2817.v | 9 ++++++ test-suite/bugs/closed/shouldsucceed/2836.v | 39 ++++++++++++++++++++++++ test-suite/complexity/ring2.v | 7 +++-- test-suite/failure/Tauto.v | 2 +- test-suite/failure/Uminus.v | 4 +-- test-suite/failure/clash_cons.v | 2 +- test-suite/failure/fixpoint1.v | 2 +- test-suite/failure/guard.v | 2 +- test-suite/failure/illtype1.v | 2 +- test-suite/failure/pattern.v | 2 +- test-suite/failure/positivity.v | 2 +- test-suite/failure/redef.v | 2 +- test-suite/failure/search.v | 2 +- test-suite/failure/subtyping2.v | 20 ++++++------ test-suite/failure/universes-buraliforti-redef.v | 20 ++++++------ test-suite/failure/universes-buraliforti.v | 20 ++++++------ test-suite/ideal-features/Apply.v | 2 +- test-suite/ideal-features/eapply_evar.v | 2 +- test-suite/micromega/example.v | 10 +++--- test-suite/micromega/square.v | 18 +++++------ test-suite/misc/berardi_test.v | 14 ++++----- test-suite/modules/PO.v | 4 +-- test-suite/modules/Przyklad.v | 14 ++++----- test-suite/output/Notations.out | 5 +++ test-suite/output/Notations.v | 9 ++++++ test-suite/output/ZSyntax.out | 14 ++++----- test-suite/success/Check.v | 2 +- test-suite/success/Field.v | 2 +- test-suite/success/Funind.v | 22 ++++++------- test-suite/success/Hints.v | 26 ++++++++-------- test-suite/success/LegacyField.v | 2 +- test-suite/success/MatchFail.v | 4 +-- test-suite/success/Mod_type.v | 12 ++++++++ test-suite/success/Notations.v | 5 +++ test-suite/success/OmegaPre.v | 16 +++++----- test-suite/success/ProgramWf.v | 6 ++-- test-suite/success/ROmegaPre.v | 16 +++++----- test-suite/success/RecTutorial.v | 10 +++--- test-suite/success/Reg.v | 8 ++--- test-suite/success/Scopes.v | 2 +- test-suite/success/Tauto.v | 2 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/Try.v | 2 +- test-suite/success/apply.v | 6 ++-- test-suite/success/change.v | 6 ++-- test-suite/success/decl_mode.v | 10 +++--- test-suite/success/dependentind.v | 2 +- test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 2 +- test-suite/success/extraction.v | 2 +- test-suite/success/fix.v | 8 ++--- test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 2 +- test-suite/success/ltac.v | 8 ++--- test-suite/success/mutual_ind.v | 2 +- test-suite/success/proof_using.v | 6 ++++ test-suite/success/remember.v | 2 +- test-suite/success/searchabout.v | 2 +- test-suite/success/setoid_test.v | 20 ++++++------ test-suite/success/specialize.v | 28 ++++++++--------- test-suite/success/unfold.v | 2 +- test-suite/success/unicode_utf8.v | 2 +- test-suite/success/univers.v | 4 +-- test-suite/typeclasses/NewSetoid.v | 2 +- 71 files changed, 296 insertions(+), 210 deletions(-) create mode 100644 test-suite/bugs/closed/shouldsucceed/2817.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2836.v (limited to 'test-suite') diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v index 3d145d96..f9821f76 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t1 | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => if (Z_ge_lt_dec h1 h2) then - if (Z_eq_dec h2 1) + if (Z.eq_dec h2 1) then add v2 s else let (l2', r2') := split v1 u in join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) else - if (Z_eq_dec h1 1) + if (Z.eq_dec h1 1) then add v1 s else let (l1', r1') := split v2 u in diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 718b0e86..fb2f0ca9 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -58,7 +58,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := match x with | I x => match y with - | I y => if (Z_eq_dec x y) then in_left else in_right + | I y => if (Z.eq_dec x y) then in_left else in_right | S ys => in_right end | S xs => diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v index 5627612f..17eeb352 100644 --- a/test-suite/bugs/closed/shouldsucceed/1844.v +++ b/test-suite/bugs/closed/shouldsucceed/1844.v @@ -1,6 +1,6 @@ Require Import ZArith. -Definition zeq := Z_eq_dec. +Definition zeq := Z.eq_dec. Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := fun y => if zeq x y then v else s y. diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v index 72396d49..d5837619 100644 --- a/test-suite/bugs/closed/shouldsucceed/1935.v +++ b/test-suite/bugs/closed/shouldsucceed/1935.v @@ -13,7 +13,7 @@ Qed. Require Import ZArith. -Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt. +Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt. Lemma f_refl'' : forall n , f'' true n n. Proof. diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v index 0fc854b6..142ada26 100644 --- a/test-suite/bugs/closed/shouldsucceed/2127.v +++ b/test-suite/bugs/closed/shouldsucceed/2127.v @@ -1,8 +1,8 @@ -(* Check that "apply refl_equal" is not exported as an interactive +(* Check that "apply eq_refl" is not exported as an interactive tactic but as a statically globalized one *) (* (this is a simplification of the original bug report) *) Module A. -Hint Rewrite sym_equal using apply refl_equal : foo. +Hint Rewrite eq_sym using apply eq_refl : foo. End A. diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v new file mode 100644 index 00000000..08dff992 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2817.v @@ -0,0 +1,9 @@ +(** Occur-check for Meta (up to application of already known instances) *) + +Goal forall (f: nat -> nat -> Prop) (x:bool) + (H: forall (u: nat), f u u -> True) + (H0: forall x0, f (if x then x0 else x0) x0), +False. + +intros. +Fail apply H in H0. (* should fail without exhausting the stack *) diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v new file mode 100644 index 00000000..a948b75e --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2836.v @@ -0,0 +1,39 @@ +(* Check that possible instantiation made during evar materialization + are taken into account and do not raise Not_found *) + +Set Implicit Arguments. + +Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := { + Object :> _ := obj; + + Identity' : forall o, Morphism o o; + Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' +}. + +Section SpecializedCategoryInterface. + Variable obj : Type. + Variable mor : obj -> obj -> Type. + Variable C : @SpecializedCategory obj mor. + + Definition Morphism (s d : C) := mor s d. + Definition Identity (o : C) : Morphism o o := C.(Identity') o. + Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) : +Morphism s d' := C.(Compose') s d d' m m0. +End SpecializedCategoryInterface. + +Section ProductCategory. + Variable objC : Type. + Variable morC : objC -> objC -> Type. + Variable objD : Type. + Variable morD : objD -> objD -> Type. + Variable C : SpecializedCategory morC. + Variable D : SpecializedCategory morD. + +(* Should fail nicely *) +Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d +=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type). +Fail refine {| + Identity' := (fun o => (Identity (fst o), Identity (snd o))); + Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd +m2) (snd m1))) + |}. diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index 6945edc8..52dae265 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -3,7 +3,7 @@ Require Import BinInt Zbool. -Definition Zplus x y := +Definition Zadd x y := match x with | 0%Z => y | Zpos x' => @@ -30,9 +30,10 @@ match x with end end. + Require Import Ring. -Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z). +Lemma Zth : ring_theory Z0 (Zpos xH) Zadd Z.mul Z.sub Z.opp (@eq Z). Admitted. Ltac Zcst t := @@ -45,7 +46,7 @@ Add Ring Zr : Zth (decidable Zeq_bool_eq, constants [Zcst]). Open Scope Z_scope. -Infix "+" := Zplus : Z_scope. +Infix "+" := Zadd : Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index a08c5154..cbe7473c 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* prop, induct i -> up (i WF). Proof. intros i y. apply y. -unfold le, WF, induct in |- *. +unfold le, WF, induct. intros x H0. apply y. exact H0. @@ -39,7 +39,7 @@ Qed. Lemma lemma1 : induct (fun u => down (I u)). Proof. -unfold induct in |- *. +unfold induct. intros x p. intro q. apply (q (fun u => down (I u)) p). diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index d000f965..25d3c165 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop. Goal forall p : n = n, P n p. intro. -pattern n, p in |- *. +pattern n, p. diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index e9fbe969..03cc1109 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* WF A Rof. - red in |- *; intros; apply ACC_inverse_image; auto. + red; intros; apply ACC_inverse_image; auto. Qed. End Inverse_Image. @@ -104,7 +104,7 @@ generalize eqx0; clear eqx0. elim eqy using eq_ind_r; intro. case (inj _ _ _ _ eqx0); intros. exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. -red in |- *; auto. +red; auto. Defined. @@ -122,7 +122,7 @@ apply sym_eq; assumption. intros. apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x))); - try red in |- *; auto. + try red; auto. Defined. (* The embedding relation is well founded *) @@ -158,7 +158,7 @@ Section Subsets. exists sub (Rof _ _ emb witness) A0 emb witness a; trivial. exact WF_emb. -red in |- *; trivial. +red; trivial. exact emb_wit. Defined. @@ -174,7 +174,7 @@ End Subsets. - the upper bound is a, which is in F(b) since a < b *) Lemma F_morphism : morphism A0 emb A0 emb F. -red in |- *; intros. +red; intros. exists (sub x) (Rof _ _ emb (witness x)) @@ -185,10 +185,10 @@ exists apply WF_inverse_image. exact WF_emb. -unfold morphism, Rof, fsub in |- *; simpl in |- *; intros. +unfold morphism, Rof, fsub; simpl; intros. trivial. -unfold Rof, fsub in |- *; simpl in |- *; intros. +unfold Rof, fsub; simpl; intros. apply emb_wit. Defined. @@ -230,10 +230,10 @@ intros. change match i0' X1 R1, i0' X2 R2 with | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f - end in |- *. -case H; simpl in |- *. + end. +case H; simpl. exists (fun x : X1 => x). -red in |- *; trivial. +red; trivial. Defined. (* The following command raises 'Error: Universe Inconsistency'. diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v index 034b7f09..a8b5b975 100644 --- a/test-suite/failure/universes-buraliforti-redef.v +++ b/test-suite/failure/universes-buraliforti-redef.v @@ -54,7 +54,7 @@ Section Inverse_Image. Qed. Lemma WF_inverse_image : WF B R -> WF A Rof. - red in |- *; intros; apply ACC_inverse_image; auto. + red; intros; apply ACC_inverse_image; auto. Qed. End Inverse_Image. @@ -106,7 +106,7 @@ generalize eqx0; clear eqx0. elim eqy using eq_ind_r; intro. case (inj _ _ _ _ eqx0); intros. exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. -red in |- *; auto. +red; auto. Defined. @@ -124,7 +124,7 @@ apply sym_eq; assumption. intros. apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x))); - try red in |- *; auto. + try red; auto. Defined. (* The embedding relation is well founded *) @@ -160,7 +160,7 @@ Section Subsets. exists sub (Rof _ _ emb witness) A0 emb witness a; trivial. exact WF_emb. -red in |- *; trivial. +red; trivial. exact emb_wit. Defined. @@ -176,7 +176,7 @@ End Subsets. - the upper bound is a, which is in F(b) since a < b *) Lemma F_morphism : morphism A0 emb A0 emb F. -red in |- *; intros. +red; intros. exists (sub x) (Rof _ _ emb (witness x)) @@ -187,10 +187,10 @@ exists apply WF_inverse_image. exact WF_emb. -unfold morphism, Rof, fsub in |- *; simpl in |- *; intros. +unfold morphism, Rof, fsub; simpl; intros. trivial. -unfold Rof, fsub in |- *; simpl in |- *; intros. +unfold Rof, fsub; simpl; intros. apply emb_wit. Defined. @@ -231,10 +231,10 @@ intros. change match i0 X1 R1, i0 X2 R2 with | i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f - end in |- *. -case H; simpl in |- *. + end. +case H; simpl. exists (fun x : X1 => x). -red in |- *; trivial. +red; trivial. Defined. (* The following command raises 'Error: Universe Inconsistency'. diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v index 1f96ab34..7b62a0c5 100644 --- a/test-suite/failure/universes-buraliforti.v +++ b/test-suite/failure/universes-buraliforti.v @@ -37,7 +37,7 @@ Section Inverse_Image. Qed. Lemma WF_inverse_image : WF B R -> WF A Rof. - red in |- *; intros; apply ACC_inverse_image; auto. + red; intros; apply ACC_inverse_image; auto. Qed. End Inverse_Image. @@ -90,7 +90,7 @@ generalize eqx0; clear eqx0. elim eqy using eq_ind_r; intro. case (inj _ _ _ _ eqx0); intros. exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. -red in |- *; auto. +red; auto. Defined. @@ -108,7 +108,7 @@ apply sym_eq; assumption. intros. apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x))); - try red in |- *; auto. + try red; auto. Defined. (* The embedding relation is well founded *) @@ -144,7 +144,7 @@ Section Subsets. exists sub (Rof _ _ emb witness) A0 emb witness a; trivial. exact WF_emb. -red in |- *; trivial. +red; trivial. exact emb_wit. Defined. @@ -160,7 +160,7 @@ End Subsets. - the upper bound is a, which is in F(b) since a < b *) Lemma F_morphism : morphism A0 emb A0 emb F. -red in |- *; intros. +red; intros. exists (sub x) (Rof _ _ emb (witness x)) @@ -171,10 +171,10 @@ exists apply WF_inverse_image. exact WF_emb. -unfold morphism, Rof, fsub in |- *; simpl in |- *; intros. +unfold morphism, Rof, fsub; simpl; intros. trivial. -unfold Rof, fsub in |- *; simpl in |- *; intros. +unfold Rof, fsub; simpl; intros. apply emb_wit. Defined. @@ -222,10 +222,10 @@ intros. change match i0 X1 R1, i0 X2 R2 with | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f - end in |- *. -case H; simpl in |- *. + end. +case H; simpl. exists (fun x : X1 => x). -red in |- *; trivial. +red; trivial. Defined. (* The following command raises 'Error: Universe Inconsistency'. diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index 8b36f44b..7628b961 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0=O. -intro H; eapply trans_equal; +intro H; eapply eq_trans; [apply H | match goal with |- ?x = ?x => reflexivity end]. Qed. diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index f424f0fc..d648c2e4 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -77,13 +77,13 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop := Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t /\ correct q t /\ rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D -> - Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s). + Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s). Proof. intros. - generalize (Zabs_eq (C p t - D q t)). - generalize (Zabs_non_eq (C p t - D q t)). - generalize (Zabs_eq (C p s -D q s)). - generalize (Zabs_non_eq (C p s - D q s)). + generalize (Z.abs_eq (C p t - D q t)). + generalize (Z.abs_neq (C p t - D q t)). + generalize (Z.abs_eq (C p s -D q s)). + generalize (Z.abs_neq (C p s - D q s)). unfold rbound2 in H. unfold rbound1 in H. intuition. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 4c00ffe4..8767f687 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -9,17 +9,17 @@ Require Import ZArith Zwf Psatz QArith. Open Scope Z_scope. -Lemma Zabs_square : forall x, (Zabs x)^2 = x^2. +Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. intros ; case (Zabs_dec x) ; intros ; psatz Z 2. Qed. -Hint Resolve Zabs_pos Zabs_square. +Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. Proof. -intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p). -assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2 - /\ Zabs p^2 = p^2) by auto. +intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p). +assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2 + /\ Z.abs p^2 = p^2) by auto. assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. @@ -35,7 +35,7 @@ Lemma QnumZpower : forall x : Q, Qnum (x ^ 2)%Q = ((Qnum x) ^ 2) %Z. Proof. intros. destruct x. - cbv beta iota zeta delta - [Zmult]. + cbv beta iota zeta delta - [Z.mul]. ring. Qed. @@ -45,15 +45,15 @@ Proof. intros. destruct x. simpl. - unfold Zpower_pos. + unfold Z.pow_pos. simpl. - rewrite Pmult_1_r. + rewrite Pos.mul_1_r. reflexivity. Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. - unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r. + unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Z.mul_1_r. intros HQeq. assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v index 2b388687..38377573 100644 --- a/test-suite/misc/berardi_test.v +++ b/test-suite/misc/berardi_test.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). Proof. intros P B e1 e2 Q p1 p2. -unfold IFProp in |- *. +unfold IFProp. case (EM B); assumption. Qed. @@ -76,7 +76,7 @@ Record retract_cond : Prop := Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. Proof. intros r. -case r; simpl in |- *. +case r; simpl. trivial. Qed. @@ -113,7 +113,7 @@ Lemma retract_pow_U_U : retract (pow U) U. Proof. exists g f. intro a. -unfold f, g in |- *; simpl in |- *. +unfold f, g; simpl. apply AC. exists (fun x:pow U => x) (fun x:pow U => x). trivial. @@ -130,8 +130,8 @@ Definition R : U := g (fun u:U => Not_b (u U u)). Lemma not_has_fixpoint : R R = Not_b (R R). Proof. -unfold R at 1 in |- *. -unfold g in |- *. +unfold R at 1. +unfold g. rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). trivial. exists (fun x:pow U => x) (fun x:pow U => x); trivial. @@ -141,7 +141,7 @@ Qed. Theorem classical_proof_irrelevence : T = F. Proof. generalize not_has_fixpoint. -unfold Not_b in |- *. +unfold Not_b. apply AC_IF. intros is_true is_false. elim is_true; elim is_false; trivial. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 71d33177..6198f29a 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -27,13 +27,13 @@ Module Pair (X: PO) (Y: PO) <: PO. Qed. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. - unfold le in |- *; intuition; info eauto. + unfold le; intuition; info eauto. Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. destruct p1. destruct p2. - unfold le in |- *. + unfold le. intuition. cutrewrite (t = t1). cutrewrite (t0 = t2). diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index e3694b81..341805a1 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -66,7 +66,7 @@ Module FuncDict (E: ELEM). Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. intros. - unfold find, add in |- *. + unfold find, add. elim (Reflexivity_provable _ _ (E.eq_dec e e)). intros. rewrite H. @@ -77,13 +77,13 @@ Module FuncDict (E: ELEM). Lemma find_add_false : forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. intros. - unfold add, find in |- *. + unfold add, find. cut (exists x : _, E.eq_dec e' e = right _ x). intros. elim H0. intros. rewrite H1. - unfold ifte in |- *. + unfold ifte. reflexivity. apply Disequality_provable. @@ -123,7 +123,7 @@ Module Lemmas (G: SET) (E: ELEM). forall a : E.T, ESet.find a S1 = ESet.find a S2. intros. - unfold S1, S2 in |- *. + unfold S1, S2. elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2; try rewrite <- H1; try rewrite <- H2; repeat @@ -153,7 +153,7 @@ Module ListDict (E: ELEM). Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true. intros. - simpl in |- *. + simpl. elim (Reflexivity_provable _ _ (E.eq_dec e e)). intros. rewrite H. @@ -165,11 +165,11 @@ Module ListDict (E: ELEM). Lemma find_add_false : forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. intros. - simpl in |- *. + simpl. elim (Disequality_provable _ _ _ H (E.eq_dec e e')). intros. rewrite H0. - simpl in |- *. + simpl. reflexivity. Qed. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index ada524f1..beba8df9 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -122,3 +122,8 @@ fun x : option Z => match x with : option Z -> Z s : s +Identifier 'foo' now a keyword +10 + : nat +fun _ : nat => 9 + : nat -> nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 4a2c411e..52f499ab 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -253,3 +253,12 @@ Check (fun x => match x with SOME3 x => x | NONE3 => 0 end). Notation s := Type. Check s. + +(* Test bug #2835: notations were not uniformly managed under prod and lambda *) + +Open Scope nat_scope. + +Notation "'foo' n" := (S n) (at level 50): nat_scope. + +Check (foo 9). +Check (fun _ : nat => 9). diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out index 1b7a2903..dc41b0aa 100644 --- a/test-suite/output/ZSyntax.out +++ b/test-suite/output/ZSyntax.out @@ -2,19 +2,19 @@ : Z fun f : nat -> Z => (f 0%nat + 0)%Z : (nat -> Z) -> Z -fun x : positive => Zpos x~0 +fun x : positive => Z.pos x~0 : positive -> Z -fun x : positive => (Zpos x + 1)%Z +fun x : positive => (Z.pos x + 1)%Z : positive -> Z -fun x : positive => Zpos x +fun x : positive => Z.pos x : positive -> Z -fun x : positive => Zneg x~0 +fun x : positive => Z.neg x~0 : positive -> Z -fun x : positive => (Zpos x~0 + 0)%Z +fun x : positive => (Z.pos x~0 + 0)%Z : positive -> Z -fun x : positive => (- Zpos x~0)%Z +fun x : positive => (- Z.pos x~0)%Z : positive -> Z -fun x : positive => (- Zpos x~0 + 0)%Z +fun x : positive => (- Z.pos x~0 + 0)%Z : positive -> Z (Z.of_nat 0 + 1)%Z : Z diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 47180ef6..21a9722d 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* iszero n = true. intros x eg. - functional induction iszero x; simpl in |- *. + functional induction iszero x; simpl. trivial. inversion eg. Qed. @@ -212,19 +212,19 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat := Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. intros a b. - functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto. + functional induction plus_x_not_five'' a b; intros hyp; simpl; auto. Qed. Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. intros n m. - functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto. + functional induction nat_equal_bool n m; simpl; intros hyp; auto. rewrite <- hyp in y; simpl in y;tauto. inversion hyp. Qed. Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. intros n m. - functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto. + functional induction nat_equal_bool n m; simpl; intros eg; auto. inversion eg. inversion eg. Qed. @@ -245,7 +245,7 @@ Qed. Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. intros n. -unfold plus in |- *. +unfold plus. functional induction plus n 0; intros. auto with arith. apply le_n_S. @@ -266,7 +266,7 @@ Function mod2 (n : nat) : nat := Lemma princ_mod2 : forall n : nat, mod2 n <= n. intros n. - functional induction mod2 n; simpl in |- *; auto with arith. + functional induction mod2 n; simpl; auto with arith. Qed. Function isfour (n : nat) : bool := @@ -284,7 +284,7 @@ Function isononeorfour (n : nat) : bool := Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). intros n. - functional induction isononeorfour n; intros istr; simpl in |- *; + functional induction isononeorfour n; intros istr; simpl; inversion istr. apply istrue0. destruct n. inversion istr. @@ -367,7 +367,7 @@ Function ftest2 (n m : nat) {struct n} : nat := Lemma test2' : forall n m : nat, ftest2 n m <= 2. intros n m. - functional induction ftest2 n m; simpl in |- *; intros; auto. + functional induction ftest2 n m; simpl; intros; auto. Qed. Function ftest3 (n m : nat) {struct n} : nat := @@ -387,7 +387,7 @@ auto. intros. auto. intros. -simpl in |- *. +simpl. auto. Qed. @@ -408,7 +408,7 @@ auto. intros. auto. intros. -simpl in |- *. +simpl. auto. Qed. @@ -451,7 +451,7 @@ Qed. Lemma essai6 : forall n m : nat, ftest6 n m <= 2. intros n m. - functional induction ftest6 n m; simpl in |- *; auto. + functional induction ftest6 n m; simpl; auto. Qed. (* Some tests with modules *) diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 071fb957..cc8cec47 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -2,26 +2,26 @@ (* Checks that qualified names are accepted *) (* New-style syntax *) -Hint Resolve refl_equal: core arith. -Hint Immediate trans_equal. -Hint Unfold sym_equal: core. +Hint Resolve eq_refl: core arith. +Hint Immediate eq_trans. +Hint Unfold eq_sym: core. Hint Constructors eq: foo bar. -Hint Extern 3 (_ = _) => apply refl_equal: foo bar. +Hint Extern 3 (_ = _) => apply eq_refl: foo bar. (* Old-style syntax *) -Hint Resolve refl_equal sym_equal. -Hint Resolve refl_equal sym_equal: foo. -Hint Immediate refl_equal sym_equal. -Hint Immediate refl_equal sym_equal: foo. -Hint Unfold fst sym_equal. -Hint Unfold fst sym_equal: foo. +Hint Resolve eq_refl eq_sym. +Hint Resolve eq_refl eq_sym: foo. +Hint Immediate eq_refl eq_sym. +Hint Immediate eq_refl eq_sym: foo. +Hint Unfold fst eq_sym. +Hint Unfold fst eq_sym: foo. (* Checks that local names are accepted *) Section A. Remark Refl : forall (A : Set) (x : A), x = x. - Proof. exact @refl_equal. Defined. - Definition Sym := sym_equal. - Let Trans := trans_equal. + Proof. exact @eq_refl. Defined. + Definition Sym := eq_sym. + Let Trans := eq_trans. Hint Resolve Refl: foo. Hint Resolve Sym: bar. diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v index df4da431..d55ae384 100644 --- a/test-suite/success/LegacyField.v +++ b/test-suite/success/LegacyField.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* fail 1 - | _ => rewrite (BinInt.Zpos_xI v) + | _ => rewrite (BinInt.Pos2Z.inj_xI v) end | |- context [(Zpos (xO ?X1))] => let v := constr:X1 in match constr:v with | 1%positive => fail 1 - | _ => rewrite (BinInt.Zpos_xO v) + | _ => rewrite (BinInt.Pos2Z.inj_xO v) end end. diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v index b847833f..d5e1a38c 100644 --- a/test-suite/success/Mod_type.v +++ b/test-suite/success/Mod_type.v @@ -17,3 +17,15 @@ Module Bar : BAR. Module Foo := Fu. End Bar. + +(* Check bug #2809: correct printing of modules with notations *) + +Module C. + Inductive test : Type := + | c1 : test + | c2 : nat -> test. + + Notation "! x" := (c2 x) (at level 50). +End C. + +Print C. (* Should print test_rect without failing *) diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 89f11059..2371d32c 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -96,3 +96,8 @@ Notation "'FORALL' x .. y , P" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity) : type_scope. Fail Check fun x => match x with S (FORALL x, _) => 0 end. + +(* Bug #2708: don't check for scope of variables used as binder *) + +Parameter traverse : (nat -> unit) -> (nat -> unit). +Notation traverse_var f l := (traverse (fun l => f l) l). diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index f4996734..17531064 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -14,38 +14,38 @@ Open Scope Z_scope. (* zify_op *) -Goal forall a:Z, Zmax a a = a. +Goal forall a:Z, Z.max a a = a. intros. omega with *. Qed. -Goal forall a b:Z, Zmax a b = Zmax b a. +Goal forall a b:Z, Z.max a b = Z.max b a. intros. omega with *. Qed. -Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c. +Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. omega with *. Qed. -Goal forall a b:Z, Zmax a b + Zmin a b = a + b. +Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. omega with *. Qed. -Goal forall a:Z, (Zabs a)*(Zsgn a) = a. +Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. intuition; subst; omega. (* pure multiplication: omega alone can't do it *) Qed. -Goal forall a:Z, Zabs a = a -> a >= 0. +Goal forall a:Z, Z.abs a = a -> a >= 0. intros. omega with *. Qed. -Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1. +Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. omega with *. Qed. @@ -119,7 +119,7 @@ Qed. (* mix of datatypes *) -Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p. +Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. omega with *. Qed. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 00a13aed..3b7f0d84 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -22,14 +22,14 @@ Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat := Print merge. -Print Zlt. +Print Z.lt. Print Zwf. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z := match n ?= m with - | Lt => Zwfrec n (Zpred m) + | Lt => Zwfrec n (Z.pred m) | _ => 0 end. diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v index bd473fa6..fa659273 100644 --- a/test-suite/success/ROmegaPre.v +++ b/test-suite/success/ROmegaPre.v @@ -14,38 +14,38 @@ Open Scope Z_scope. (* zify_op *) -Goal forall a:Z, Zmax a a = a. +Goal forall a:Z, Z.max a a = a. intros. romega with *. Qed. -Goal forall a b:Z, Zmax a b = Zmax b a. +Goal forall a b:Z, Z.max a b = Z.max b a. intros. romega with *. Qed. -Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c. +Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. romega with *. Qed. -Goal forall a b:Z, Zmax a b + Zmin a b = a + b. +Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. romega with *. Qed. -Goal forall a:Z, (Zabs a)*(Zsgn a) = a. +Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. intuition; subst; romega. (* pure multiplication: omega alone can't do it *) Qed. -Goal forall a:Z, Zabs a = a -> a >= 0. +Goal forall a:Z, Z.abs a = a -> a >= 0. intros. romega with *. Qed. -Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1. +Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. romega with *. Qed. @@ -119,7 +119,7 @@ Qed. (* mix of datatypes *) -Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p. +Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. romega with *. Qed. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 64048fe2..459645f6 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -378,18 +378,18 @@ Inductive itree : Set := Definition isingle l := inode l (fun i => ileaf). -Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))). +Definition t1 := inode 0 (fun n => isingle (Z.of_nat (2*n))). Definition t2 := inode 0 (fun n : nat => - inode (Z_of_nat n) - (fun p => isingle (Z_of_nat (n*p)))). + inode (Z.of_nat n) + (fun p => isingle (Z.of_nat (n*p)))). Inductive itree_le : itree-> itree -> Prop := | le_leaf : forall t, itree_le ileaf t | le_node : forall l l' s s', - Zle l l' -> + Z.le l l' -> (forall i, exists j:nat, itree_le (s i) (s' j)) -> itree_le (inode l s) (inode l' s'). @@ -424,7 +424,7 @@ Qed. Inductive itree_le' : itree-> itree -> Prop := | le_leaf' : forall t, itree_le' ileaf t | le_node' : forall l l' s s' g, - Zle l l' -> + Z.le l l' -> (forall i, itree_le' (s i) (s' (g i))) -> itree_le' (inode l s) (inode l' s'). diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v index 89b3032c..c2d5cb2f 100644 --- a/test-suite/success/Reg.v +++ b/test-suite/success/Reg.v @@ -39,7 +39,7 @@ Lemma essai7 : derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1. reg. apply Rlt_0_1. -red in |- *; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0; +red; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0; assumption. Qed. @@ -127,7 +127,7 @@ Lemma essai23 : (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1. reg. left; apply Rlt_0_1. -right; unfold Rminus in |- *; rewrite Rplus_opp_r; reflexivity. +right; unfold Rminus; rewrite Rplus_opp_r; reflexivity. Qed. Lemma essai24 : @@ -135,8 +135,8 @@ Lemma essai24 : reg. replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R. apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ]. -unfold Rsqr in |- *; ring. -red in |- *; intro; cut (0 < x * x + 1)%R. +unfold Rsqr; ring. +red; intro; cut (0 < x * x + 1)%R. intro; rewrite H in H0; elim (Rlt_irrefl _ H0). apply Rplus_le_lt_0_compat; [ replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ] diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 55d8343e..a79d28fa 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -3,6 +3,6 @@ Require Import ZArith. Module A. -Definition opp := Zopp. +Definition opp := Z.opp. End A. Check (A.opp 3). diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index c4e67677..73ef3720 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* x * z < y * z -> x <= y)%Z. -intros; apply Znot_le_gt, Zgt_lt in H. -apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. +intros; apply Znot_le_gt, Z.gt_lt in H. +apply Zmult_lt_reg_r, Z.lt_le_incl in H0; auto. Qed. (* Test application under tuples *) @@ -266,7 +266,7 @@ Qed. (* This works because unfold calls clos_norm_flags which calls nf_evar *) Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O. -intros x H; eapply trans_equal; +intros x H; eapply eq_trans; [apply H | unfold x;match goal with |- ?x = ?x => reflexivity end]. Qed. diff --git a/test-suite/success/change.v b/test-suite/success/change.v index c65cf303..7bed7ecb 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -14,7 +14,7 @@ Abort. (* Check the combination of at, with and in (see bug #2146) *) Goal 3=3 -> 3=3. intro H. -change 3 at 2 with (1+2) in |- *. +change 3 at 2 with (1+2). change 3 at 2 with (1+2) in H |-. change 3 with (1+2) in H at 1 |- * at 1. (* Now check that there are no more 3's *) @@ -25,10 +25,10 @@ Qed. change 3 at 1 with (1+2) at 3. change 3 at 1 with (1+2) in *. change 3 at 1 with (1+2) in H at 2 |-. -change 3 at 1 with (1+2) in |- * at 3. +change 3 at 1 with (1+2) at 3. change 3 at 1 with (1+2) in H |- *. change 3 at 1 with (1+2) in H, H|-. -change 3 in |- * at 1. +change 3 at 1. *) (* Test that pretyping checks allowed elimination sorts *) diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v index bc1757fd..52575eca 100644 --- a/test-suite/success/decl_mode.v +++ b/test-suite/success/decl_mode.v @@ -138,7 +138,7 @@ Coercion IZR: Z >->R.*) Open Scope R_scope. Lemma square_abs_square: - forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p). + forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p). proof. assume p:Z. per cases on p. @@ -147,7 +147,7 @@ proof. suppose it is (Zpos z). thus thesis. suppose it is (Zneg z). - have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) = + have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) = (IZR (Zpos z) * IZR (Zpos z))). ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))). thus ~= (IZR (Zneg z) * IZR (Zneg z)). @@ -165,15 +165,15 @@ proof. have H_in_R:(INR q<>0:>R) by H. have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field. have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def. - have (INR (Zabs_nat p * Zabs_nat p) - = (INR (Zabs_nat p) * INR (Zabs_nat p))) + have (INR (Z.abs_nat p * Z.abs_nat p) + = (INR (Z.abs_nat p) * INR (Z.abs_nat p))) by mult_INR. ~= (IZR p* IZR p) by square_abs_square. ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *) ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring. ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0. ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR. - then (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat. + then (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat. ~= ((q*q)+(q*q))%nat. ~= (Div2.double (q*q)). then (q=0%nat) by main_theorem. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 79d12a06..12ddbda8 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -68,7 +68,7 @@ where " Γ ⊢ τ " := (term Γ τ) : type_scope. Hint Constructors term : lambda. -Open Local Scope context_scope. +Local Open Scope context_scope. Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index a94d8b1d..49bf8b15 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* x + x + x = 3. intros x H. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index fcadd150..5fe760bf 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop), P nat 0 -> P nat 0. intros. Fail remember nat as X. Fail remember nat as X in H. (* This line used to succeed in 8.3 *) -Fail remember nat as X in |- *. +Fail remember nat as X. Abort. diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v index d9ade314..9edfd825 100644 --- a/test-suite/success/searchabout.v +++ b/test-suite/success/searchabout.v @@ -55,6 +55,6 @@ SearchAbout [-"*"%nat "+"%nat] outside Logic. Require Import ZArith. -SearchAbout Zmult Zplus "distr". +SearchAbout Z.mul Z.add "distr". SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 19693d70..653b5bf9 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -18,10 +18,10 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t. Lemma setoid_set : Setoid_Theory set same. -unfold same in |- *; split ; red. -red in |- *; auto. +unfold same; split ; red. +red; auto. -red in |- *. +red. intros. elim (H a); auto. @@ -33,19 +33,19 @@ Qed. Add Setoid set same setoid_set as setsetoid. Add Morphism In : In_ext. -unfold same in |- *; intros a s t H; elim (H a); auto. +unfold same; intros a s t H; elim (H a); auto. Qed. Lemma add_aux : forall s t : set, same s t -> forall a b : A, In a (Add b s) -> In a (Add b t). -unfold same in |- *; simple induction 2; intros. +unfold same; simple induction 2; intros. rewrite H1. -simpl in |- *; left; reflexivity. +simpl; left; reflexivity. elim (H a). intros. -simpl in |- *; right. +simpl; right. apply (H2 H1). Qed. @@ -74,15 +74,15 @@ setoid_replace (remove a (Add a Empty)) with Empty. auto. -unfold same in |- *. +unfold same. split. -simpl in |- *. +simpl. case (eq_dec a a). intros e ff; elim ff. intros; absurd (a = a); trivial. -simpl in |- *. +simpl. intro H; elim H. Qed. diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 57837321..c5f032be 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -5,20 +5,20 @@ intros. (* "compatibility" mode: specializing a global name means a kind of generalize *) -specialize trans_equal. intros _. -specialize trans_equal with (1:=H)(2:=H0). intros _. -specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _. -specialize trans_equal with (1:=H)(z:=c). intros _. -specialize trans_equal with nat a b c. intros _. -specialize (@trans_equal nat). intros _. -specialize (@trans_equal _ a b c). intros _. -specialize (trans_equal (x:=a)). intros _. -specialize (trans_equal (x:=a)(y:=b)). intros _. -specialize (trans_equal H H0). intros _. -specialize (trans_equal H0 (z:=b)). intros _. +specialize eq_trans. intros _. +specialize eq_trans with (1:=H)(2:=H0). intros _. +specialize eq_trans with (x:=a)(y:=b)(z:=c). intros _. +specialize eq_trans with (1:=H)(z:=c). intros _. +specialize eq_trans with nat a b c. intros _. +specialize (@eq_trans nat). intros _. +specialize (@eq_trans _ a b c). intros _. +specialize (eq_trans (x:=a)). intros _. +specialize (eq_trans (x:=a)(y:=b)). intros _. +specialize (eq_trans H H0). intros _. +specialize (eq_trans H0 (z:=b)). intros _. (* local "in place" specialization *) -assert (Eq:=trans_equal). +assert (Eq:=eq_trans). specialize Eq. specialize Eq with (1:=H)(2:=H0). Undo. @@ -38,10 +38,10 @@ specialize (Eq _ _ _ b H0). Undo. presque ok... *) (* 2) echoue moins lorsque zero premise de mangé *) -specialize trans_equal with (1:=Eq). (* mal typé !! *) +specialize eq_trans with (1:=Eq). (* mal typé !! *) (* 3) *) -specialize trans_equal with _ a b c. intros _. +specialize eq_trans with _ a b c. intros _. (* Anomaly: Evar ?88 was not declared. Please report. *) *) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 5649e2f7..62ecb1aa 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*