diff options
Diffstat (limited to 'test-suite/success')
37 files changed, 140 insertions, 117 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 0efd90a1..9301cd27 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index b17adef6..ccce3bbe 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -9,7 +9,7 @@ Functional Scheme iszero_ind := Induction for iszero Sort Prop. Lemma toto : forall n : nat, n = 0 -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index 660ca3cb..c2d87a44 100644 --- a/test-suite/success/MatchFail.v +++ b/test-suite/success/MatchFail.v @@ -12,13 +12,13 @@ Ltac compute_POS := let v := constr:X1 in match constr:v with | 1%positive => 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 705bdc45..e9d6a969 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v index b356f277..361c787e 100644 --- a/test-suite/success/Try.v +++ b/test-suite/success/Try.v @@ -2,7 +2,7 @@ non-existent names in Unfold [cf bug #263] *) Lemma lem1 : True. -try unfold i_dont_exist in |- *. +try unfold i_dont_exist. trivial. Qed. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index d3c76101..0d8bf556 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -8,8 +8,8 @@ Qed. Require Import ZArith. Goal (forall x y z, ~ z <= 0 -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 8c00583e..df73383a 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 3f8a3bc4..acd1da66 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index b25b502c..8623f718 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -9,16 +9,16 @@ Inductive rBoolOp : Set := | rAnd : rBoolOp | rEq : rBoolOp. -Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt. +Definition rlt (a b : rNat) : Prop := Pos.compare_cont a b Eq = Lt. Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}. intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m); generalize (nat_of_P_gt_Gt_compare_morphism n m); - generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq). + generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq). intros H' H'0 H'1; right; right; auto. -intros H' H'0 H'1; left; unfold rlt in |- *. +intros H' H'0 H'1; left; unfold rlt. apply nat_of_P_lt_Lt_compare_complement_morphism; auto. -intros H' H'0 H'1; right; left; unfold rlt in |- *. +intros H' H'0 H'1; right; left; unfold rlt. apply nat_of_P_lt_Lt_compare_complement_morphism; auto. apply H'0; auto. Defined. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 234c4223..9316ac03 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index b24ed2f1..cc8e8dd8 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 7387add6..c2eb8bd7 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -2,7 +2,7 @@ (* Submitted by Pierre Crégut *) (* Checks substitution of x *) -Ltac f x := unfold x in |- *; idtac. +Ltac f x := unfold x; idtac. Lemma lem1 : 0 + 0 = 0. f plus. @@ -86,7 +86,7 @@ assert t. exact H. intro H1. apply H. -symmetry in |- *. +symmetry . assumption. Qed. @@ -105,7 +105,7 @@ sym'. exact H. intro H1. apply H. -symmetry in |- *. +symmetry . assumption. Qed. @@ -193,7 +193,7 @@ Abort. (* Used to fail in V8.1 *) Tactic Notation "test" constr(t) integer(n) := - set (k := t) in |- * at n. + set (k := t) at n. Goal forall x : nat, x = 1 -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index 93a9ef11..bf302df4 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -51,11 +51,17 @@ Proof using v1 v2. admit. Qed. +Lemma deep2 : v1 = v2. +Proof using v1 v2. +Admitted. + End S2. Check (deep 3 : v1 = 3). +Check (deep2 3 : v1 = 3). End S1. Check (deep 3 4 : 3 = 4). +Check (deep2 3 4 : 3 = 4). diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v index 3241e133..5f8ed03d 100644 --- a/test-suite/success/remember.v +++ b/test-suite/success/remember.v @@ -4,5 +4,5 @@ Lemma A : forall (P: forall X, X -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index 8b7764e5..42e32ccc 100644 --- a/test-suite/success/unicode_utf8.v +++ b/test-suite/success/unicode_utf8.v @@ -75,7 +75,7 @@ Notation "x ≤ y" := (x<=y) (at level 70, no associativity). Require Import ZArith. Open Scope Z_scope. -Locate "≤". (* still le, not Zle *) +Locate "≤". (* still le, not Z.le *) Notation "x ≤ y" := (x<=y) (at level 70, no associativity). Locate "≤". Close Scope Z_scope. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 469cbeb7..e00701fb 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -16,7 +16,7 @@ auto. Qed. Lemma lem3 : forall P : Prop, P. -intro P; pattern P in |- *. +intro P; pattern P. apply lem2. Abort. @@ -34,7 +34,7 @@ Require Import Relations. Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X). Proof. - unfold transitive in |- *. + unfold transitive. intros X f g h H1 H2. inversion H1. Abort. |