diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_2083.v | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_3652.v | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4280.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4306.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4456.v | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4852.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/opened/bug_1596.v | 6 | ||||
| -rw-r--r-- | test-suite/complexity/pattern.v | 2 | ||||
| -rw-r--r-- | test-suite/modules/PO.v | 4 | ||||
| -rw-r--r-- | test-suite/output/Fixpoint.v | 8 | ||||
| -rw-r--r-- | test-suite/success/CanonicalStructure.v | 22 | ||||
| -rw-r--r-- | test-suite/success/LocalDefinition.v | 28 | ||||
| -rw-r--r-- | test-suite/success/NotationDeprecation.v | 24 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 9 |
15 files changed, 62 insertions, 83 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1744138d29..609a61226b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -543,13 +543,15 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) res=`echo "$$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`; \ true "find expected time * 100"; \ exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \ + true "compute corrected effective time, rounded up"; \ + rescorrected=`expr \( $$res \* $(bogomips) \+ 6120 \- 1 \) \/ 6120`; \ ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \ if [ "$$ok" = 1 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " $<...Error! (should run faster)"; \ + echo " $<...Error! (should run faster ($$rescorrected >= $$exp))"; \ $(FAIL); \ fi; \ fi; \ diff --git a/test-suite/bugs/closed/bug_2083.v b/test-suite/bugs/closed/bug_2083.v index f33e96cea6..40fda71e66 100644 --- a/test-suite/bugs/closed/bug_2083.v +++ b/test-suite/bugs/closed/bug_2083.v @@ -13,15 +13,15 @@ Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) error end. -Require Import Omega. +Require Import Lia. -Solve Obligations with program_simpl ; auto with *; try omega. +Solve Obligations with program_simpl ; auto with *; lia. Next Obligation. - apply H. simpl. omega. + apply H. simpl. lia. Defined. Next Obligation. - case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. + case (le_lt_dec p i) ; intros. assert(i = p) by lia. subst. revert H0. clear_subset_proofs. auto. apply H. simpl. assumption. Defined. diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v index 915cfcac27..b21a4d939c 100644 --- a/test-suite/bugs/closed/bug_3652.v +++ b/test-suite/bugs/closed/bug_3652.v @@ -1,6 +1,7 @@ Require Setoid. Require ZArith. Import ZArith. +Require Import Lia. Inductive Erasable(A : Set) : Prop := erasable: A -> Erasable A. @@ -87,12 +88,12 @@ Proof. unfold zotval. unfold mp2a1s. ring_simplify'. - replace 2 with (2*1) at 2 7 by omega. + replace 2 with (2*1) at 2 7 by lia. rewrite <-?Z.mul_assoc. rewrite <-?Z.mul_add_distr_l. rewrite <-Z.mul_sub_distr_l. - rewrite Z.mul_cancel_l by omega. - replace 1 with (2-1) at 1 by omega. + rewrite Z.mul_cancel_l by lia. + replace 1 with (2-1) at 1 by lia. rewrite Z.add_sub_assoc. rewrite Z.sub_cancel_r. Unshelve. diff --git a/test-suite/bugs/closed/bug_4280.v b/test-suite/bugs/closed/bug_4280.v index fd7897509e..31524e5dcf 100644 --- a/test-suite/bugs/closed/bug_4280.v +++ b/test-suite/bugs/closed/bug_4280.v @@ -1,11 +1,11 @@ -Require Import ZArith. +Require Import ZArith Lia. Require Import Eqdep_dec. Local Open Scope Z_scope. Definition t := { n: Z | n > 1 }. Program Definition two : t := 2. -Next Obligation. omega. Qed. +Next Obligation. lia. Qed. Program Definition t_eq (x y: t) : {x=y} + {x<>y} := if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _. diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v index f1bce04451..1ad84f9bb5 100644 --- a/test-suite/bugs/closed/bug_4306.v +++ b/test-suite/bugs/closed/bug_4306.v @@ -1,7 +1,7 @@ Require Import List. Require Import Arith. Require Import Recdef. -Require Import Omega. +Require Import Lia. Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := match xys with @@ -14,9 +14,7 @@ Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) end end. Proof. - intros; simpl; omega. - intros; simpl; omega. - intros; simpl; omega. + all: simpl; lia. Qed. Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v index 7685552725..0c26d4de32 100644 --- a/test-suite/bugs/closed/bug_4456.v +++ b/test-suite/bugs/closed/bug_4456.v @@ -10,7 +10,7 @@ Tactic Notation "admit" := case proof_admitted. Require Coq.Program.Program. Require Coq.Strings.String. -Require Coq.omega.Omega. +Require Coq.micromega.Lia. Module Export Fiat_DOT_Common. Module Export Fiat. Module Common. @@ -489,7 +489,8 @@ Defined. End app. Import Coq.Lists.List. -Import Coq.omega.Omega. +Import Coq.Arith.Arith. +Import Coq.micromega.Lia. Import Fiat_DOT_Common.Fiat.Common. Import Fiat.Parsers.ContextFreeGrammar.Valid. Local Open Scope string_like_scope. @@ -585,8 +586,8 @@ Defined. | _ => discriminate | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) | _ => solve [ eauto with nocore ] - | _ => solve [ apply Min.min_case_strong; omega ] - | _ => omega + | _ => solve [ apply Min.min_case_strong; lia ] + | _ => lia | [ H : production_valid (_::_) |- _ ] => let H' := fresh in pose proof H as H'; diff --git a/test-suite/bugs/closed/bug_4852.v b/test-suite/bugs/closed/bug_4852.v index e2e00f05d3..cdc8cd8b20 100644 --- a/test-suite/bugs/closed/bug_4852.v +++ b/test-suite/bugs/closed/bug_4852.v @@ -2,7 +2,7 @@ Require Import Coq.Lists.List. Import ListNotations. -Require Import Omega. +Require Import Lia. Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf. @@ -16,7 +16,7 @@ Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) := Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws. -Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega. +Ltac solve_nat := autorewrite with app_rws in *; cbn in *; lia. Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'"). diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 27cb731151..89410047b2 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -1,7 +1,7 @@ Require Import Relations. Require Import FSets. Require Import Arith. -Require Import Omega. +Require Import Lia. Set Keyed Unification. @@ -147,14 +147,14 @@ Module MessageSpi. Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z). unfold lt. induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros. - omega. + lia. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). unfold eq;unfold lt. induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate H0);injection H0;intros. - elim (lt_irrefl n);try omega. + elim (lt_irrefl n); lia. Qed. Definition compare : forall (x y:t),(Compare lt eq x y). diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v index fb5bf5a00b..2101535be7 100644 --- a/test-suite/complexity/pattern.v +++ b/test-suite/complexity/pattern.v @@ -1,5 +1,5 @@ (** Testing the performance of [pattern]. For not regressing on COQBUG(https://github.com/coq/coq/issues/11150) and COQBUG(https://github.com/coq/coq/issues/6502) *) -(* Expected time < 0.75s *) +(* Expected time < 1.65s *) (* reference: 0.673s after adjustment *) Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v := let x := v in f x. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index be33104918..4c0ee1b5bd 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -35,8 +35,8 @@ Module Pair (X: PO) (Y: PO) <: PO. destruct p2. unfold le. intuition. - cutrewrite (t = t1). - cutrewrite (t0 = t2). + enough (t = t1) as ->. + enough (t0 = t2) as ->. reflexivity. info auto. diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..398528de72 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -16,7 +16,7 @@ Check end in f 0. -Require Import ZArith_base Omega. +Require Import ZArith_base Lia. Open Scope Z_scope. Inductive even: Z -> Prop := @@ -35,13 +35,13 @@ Proof. fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). intros. destruct H. - omega. + lia. apply odd_pos_even_pos in H. - omega. + lia. intros. destruct H. apply even_pos_odd_pos in H. - omega. + lia. Qed. CoInductive Inf := S { projS : Inf }. diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index b8cae47196..e6d674c1e6 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -29,3 +29,25 @@ Canonical Structure bool_test := mk_test (fun x y => x || y). Definition b := bool. Check (fun x : b => x != x). + +Inductive four := x0 | x1 | x2 | x3. +Structure local := MKL { l : four }. + +Section X. + Definition s0 := MKL x0. + #[local] Canonical Structure s0. + Check (refl_equal _ : l _ = x0). + + #[local] Canonical Structure s1 := MKL x1. + Check (refl_equal _ : l _ = x1). + + Local Canonical Structure s2 := MKL x2. + Check (refl_equal _ : l _ = x2). + +End X. +Fail Check (refl_equal _ : l _ = x0). +Fail Check (refl_equal _ : l _ = x1). +Fail Check (refl_equal _ : l _ = x2). +Check s0. +Check s1. +Check s2. diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v index 22fb09526d..d944036112 100644 --- a/test-suite/success/LocalDefinition.v +++ b/test-suite/success/LocalDefinition.v @@ -26,28 +26,12 @@ Module TestAdmittedVisibility. Fail Check d2. End TestAdmittedVisibility. -(* Test consistent behavior of Local Definition wrt automatic declaration of instances *) - Module TestVariableAsInstances. - Module Test1. - Set Typeclasses Axioms Are Instances. - Class U. - Local Parameter b : U. - Definition testU := _ : U. (* _ resolved *) - - Class T. - Variable a : T. (* warned to be the same as "Local Parameter" *) - Definition testT := _ : T. (* _ resolved *) - End Test1. - - Module Test2. - Unset Typeclasses Axioms Are Instances. - Class U. - Local Parameter b : U. - Fail Definition testU := _ : U. (* _ unresolved *) + Class U. + Local Parameter b : U. + Fail Definition testU := _ : U. (* _ unresolved *) - Class T. - Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) - Fail Definition testT := _ : T. (* used to succeed *) - End Test2. + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) + Fail Definition testT := _ : T. (* used to succeed *) End TestVariableAsInstances. diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v index 96814a1b97..60d40d3d12 100644 --- a/test-suite/success/NotationDeprecation.v +++ b/test-suite/success/NotationDeprecation.v @@ -3,19 +3,11 @@ Module Syndefs. #[deprecated(since = "8.9", note = "Do not use.")] Notation foo := Prop. -Notation bar := Prop (compat "8.9"). - -Fail -#[deprecated(since = "8.9", note = "Do not use.")] -Notation zar := Prop (compat "8.9"). - Check foo. -Check bar. Set Warnings "+deprecated". Fail Check foo. -Fail Check bar. End Syndefs. @@ -24,19 +16,11 @@ Module Notations. #[deprecated(since = "8.9", note = "Do not use.")] Notation "!!" := Prop. -Notation "##" := Prop (compat "8.9"). - -Fail -#[deprecated(since = "8.9", note = "Do not use.")] -Notation "**" := Prop (compat "8.9"). - Check !!. -Check ##. Set Warnings "+deprecated". Fail Check !!. -Fail Check ##. End Notations. @@ -45,18 +29,10 @@ Module Infix. #[deprecated(since = "8.9", note = "Do not use.")] Infix "!!" := plus (at level 1). -Infix "##" := plus (at level 1, compat "8.9"). - -Fail -#[deprecated(since = "8.9", note = "Do not use.")] -Infix "**" := plus (at level 1, compat "8.9"). - Check (_ !! _). -Check (_ ## _). Set Warnings "+deprecated". Fail Check (_ !! _). -Fail Check (_ ## _). End Infix. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 736d05fefc..3f96bf2c35 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -241,13 +241,8 @@ Module IterativeDeepening. End IterativeDeepening. -Module AxiomsAreInstances. - Set Typeclasses Axioms Are Instances. - Class TestClass1 := {}. - Axiom testax1 : TestClass1. - Definition testdef1 : TestClass1 := _. +Module AxiomsAreNotInstances. - Unset Typeclasses Axioms Are Instances. Class TestClass2 := {}. Axiom testax2 : TestClass2. Fail Definition testdef2 : TestClass2 := _. @@ -256,4 +251,4 @@ Module AxiomsAreInstances. Existing Instance testax2. Definition testdef2 : TestClass2 := _. -End AxiomsAreInstances. +End AxiomsAreNotInstances. |