diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12529.v | 21 | ||||
| -rw-r--r-- | test-suite/micromega/zify.v | 11 |
2 files changed, 31 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_12529.v b/test-suite/bugs/closed/bug_12529.v new file mode 100644 index 0000000000..bc3c9a28bd --- /dev/null +++ b/test-suite/bugs/closed/bug_12529.v @@ -0,0 +1,21 @@ +Goal SProp. +match goal with |- SProp => idtac end. +Fail match goal with |- Prop => idtac end. +Abort. + +Goal Prop. +Fail match goal with |- SProp => idtac end. +match goal with |- Prop => idtac end. +Abort. + +Class F A := f : A. + +Inductive pFalse : Prop := . +Inductive sFalse : SProp := . + +Hint Extern 0 (F Prop) => exact pFalse : typeclass_instances. +Definition pf := f : Prop. + +Hint Extern 0 (F SProp) => exact sFalse : typeclass_instances. +Definition sf := (f : SProp). +Definition pf' := (f : Prop). diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v index 8fd7398638..a12623c3c0 100644 --- a/test-suite/micromega/zify.v +++ b/test-suite/micromega/zify.v @@ -159,7 +159,7 @@ Require Import ZifyClasses. Require Import ZifyInst. Instance Zero : CstOp (@zero znat : nat) := Op_O. -Add CstOp Zero. +Add Zify CstOp Zero. Goal @zero znat = 0%nat. @@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0. Proof. intros. lia. Qed. + +Ltac Zify.zify_pre_hook ::= unfold is_true in *. + +Goal forall x y : nat, is_true (Nat.eqb x 1) -> + is_true (Nat.eqb y 0) -> + is_true (Nat.eqb (x + y) 1). +Proof. +lia. +Qed. |