diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_11866.v | 43 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_14131.v | 19 | ||||
| -rw-r--r-- | test-suite/ltac2/std_tactics.v | 29 | ||||
| -rw-r--r-- | test-suite/micromega/bug_11089.v | 13 | ||||
| -rw-r--r-- | test-suite/micromega/zify.v | 7 |
5 files changed, 111 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11866.v b/test-suite/bugs/closed/bug_11866.v new file mode 100644 index 0000000000..5a47f3833e --- /dev/null +++ b/test-suite/bugs/closed/bug_11866.v @@ -0,0 +1,43 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Notation "ex0" x(tactic(0)) := (). +Ltac2 Notation "ex1" x(tactic(1)) := (). +Ltac2 Notation "ex2" x(tactic(2)) := (). +Ltac2 Notation "ex3" x(tactic(3)) := (). +Ltac2 Notation "ex4" x(tactic(4)) := (). +Ltac2 Notation "ex5" x(tactic(5)) := (). +Ltac2 Notation "ex6" x(tactic(6)) := (). + +Ltac2 Notation ":::0" x(tactic) "+0" y(tactic) : 0 := (). +Ltac2 Notation ":::1" x(tactic) "+1" y(tactic) : 1 := (). +Ltac2 Notation ":::2" x(tactic) "+2" y(tactic) : 2 := (). +Ltac2 Notation ":::3" x(tactic) "+3" y(tactic) : 3 := (). +Ltac2 Notation ":::4" x(tactic) "+4" y(tactic) : 4 := (). +Ltac2 Notation ":::5" x(tactic) "+5" y(tactic) : 5 := (). +Ltac2 Notation ":::6" x(tactic) "+6" y(tactic) : 6 := (). +Fail Ltac2 Notation ":::7" x(tactic) "+7" y(tactic) : 7 := (). +Goal True. + ex0 :::0 0 +0 0. + ex1 :::0 0 +0 0. + (*ex2 :::0 0 +0 0.*) (* fails with an anomaly, cf COQBUG(https://github.com/coq/coq/issues/12807) *) + (*ex3 :::0 0 +0 0.*) + ex4 :::0 0 +0 0. + ex5 :::0 0 +0 0. + ex6 :::0 0 +0 0. + + ex0 :::1 0 +1 0. + ex1 :::1 0 +1 0. + (*ex2 :::1 0 +1 0.*) + (*ex3 :::1 0 +1 0.*) + ex4 :::1 0 +1 0. + ex5 :::1 0 +1 0. + ex6 :::1 0 +1 0. + + ex0 :::6 0 +6 0. + ex1 :::6 0 +6 0. + (*ex2 :::6 0 +6 0.*) + (*ex3 :::6 0 +6 0.*) + ex4 :::6 0 +6 0. + ex5 :::6 0 +6 0. + ex6 :::6 0 +6 0. +Abort. diff --git a/test-suite/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v new file mode 100644 index 0000000000..611464458e --- /dev/null +++ b/test-suite/bugs/closed/bug_14131.v @@ -0,0 +1,19 @@ +Set Implicit Arguments. +Unset Elimination Schemes. + +Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := + JMeq_refl : JMeq x x. + +Set Elimination Schemes. + +Register JMeq as core.JMeq.type. + +Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq x y -> P y. + +Register JMeq_ind as core.JMeq.ind. + +Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), + P x -> forall y, JMeq y x -> P y. +Proof. intros. try rewrite H0. +Abort. diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v new file mode 100644 index 0000000000..39b620a6ac --- /dev/null +++ b/test-suite/ltac2/std_tactics.v @@ -0,0 +1,29 @@ +Require Import Ltac2.Ltac2. + +Axiom f: nat -> nat. +Definition g := f. + +Axiom Foo1: nat -> Prop. +Axiom Foo2: nat -> Prop. +Axiom Impl: forall n: nat, Foo1 (f n) -> Foo2 (f n). + +Create HintDb foo discriminated. +#[export] Hint Constants Opaque : foo. +#[export] Hint Resolve Impl : foo. + +Goal forall x, Foo1 (f x) -> Foo2 (g x). +Proof. + auto with foo. + #[export] Hint Transparent g : foo. + auto with foo. +Qed. + +Goal forall (x: nat), exists y, f x = g y. +Proof. + intros. + eexists. + unify f g. + lazy_match! goal with + | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs + end. +Abort. diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v new file mode 100644 index 0000000000..e62b5b8d9e --- /dev/null +++ b/test-suite/micromega/bug_11089.v @@ -0,0 +1,13 @@ +Require Import Lia. +Unset Lia Cache. +Definition t := nat. +Goal forall (n : t), n = n. +Proof. + intros. + lia. +Qed. +Goal let t' := nat in forall (n : t'), n = n. +Proof. + intros. + lia. +Qed. diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v index a12623c3c0..2ea320047d 100644 --- a/test-suite/micromega/zify.v +++ b/test-suite/micromega/zify.v @@ -167,6 +167,12 @@ Goal @zero znat = 0%nat. reflexivity. Qed. +Require Import ZifyBool. +Instance Op_bool_inj : UnOp (inj : bool -> bool) := + { TUOp := id; TUOpInj := fun _ => eq_refl }. +Add Zify UnOp Op_bool_inj. + + Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y), (F P + 1 = 1 + F P)%positive. Proof. @@ -228,6 +234,7 @@ Proof. intros. lia. Qed. + Ltac Zify.zify_pre_hook ::= unfold is_true in *. Goal forall x y : nat, is_true (Nat.eqb x 1) -> |