diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12228.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12529.v | 21 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12532.v | 56 | ||||
| -rw-r--r-- | test-suite/micromega/zify.v | 11 |
5 files changed, 99 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index d4ad438d61..59cc3e5a38 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -629,7 +629,14 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG } > "$@" # Additional dependencies for module tests -$(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo +COMMON_MODULE_DEPENDENCIES := modules/plik.v modules/Nat.v +# We exclude Nat.v.log and plik.v.log because these log files do not +# depend on having the corresponding .vo files built first, and we end +# up with pseudo-cyclic build rules if we don't exclude them (See +# COQBUG(https://github.com/coq/coq/issues/12582)). Additionally, we +# impose order-only dependencies to ensure that we won't rebuild the +# .vo files in the .log target after we've already built them. +$(addsuffix .log,$(filter-out $(COMMON_MODULE_DEPENDENCIES),$(wildcard modules/*.v))): %.v.log: $(COMMON_MODULE_DEPENDENCIES:.v=.vo) | $(COMMON_MODULE_DEPENDENCIES:.v=.v.log) modules/%.vo: modules/%.v $(HIDE)$(coqc) -R modules Mods $< diff --git a/test-suite/bugs/closed/bug_12228.v b/test-suite/bugs/closed/bug_12228.v new file mode 100644 index 0000000000..a874fa0570 --- /dev/null +++ b/test-suite/bugs/closed/bug_12228.v @@ -0,0 +1,4 @@ +Tactic Notation "mark" constr(P) "at" integer_list(L) := pattern P at L. +Goal 0 = 0. +mark 0 at -2. +Abort. 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/bugs/closed/bug_12532.v b/test-suite/bugs/closed/bug_12532.v new file mode 100644 index 0000000000..665f6643e6 --- /dev/null +++ b/test-suite/bugs/closed/bug_12532.v @@ -0,0 +1,56 @@ +(** This is a change of behaviour introduced by PR #12532. It is not clear + whether it is a legit behaviour but it is worth having it in the test + suite. *) + +Module Foo. + +Axiom whatever : Type. +Axiom name : Type. +Axiom nw : forall (P : Type), name -> P. +Axiom raft_data : Type. +Axiom In : raft_data -> Prop. + +Axiom foo : forall st st', In st -> In st'. + +Definition params := prod whatever raft_data. + +Goal forall + (d : raft_data), + (forall (h : name), In (@snd whatever raft_data (@nw params h))) -> + In d. +Proof. +intros. +eapply foo. +solve [debug eauto]. +Abort. + +End Foo. + +Module Bar. + +Axiom whatever : Type. +Axiom AppendEntries : whatever -> Prop. +Axiom name : Type. +Axiom nw : forall (P : Type), name -> P. +Axiom raft_data : Type. +Axiom In : raft_data -> Prop. + +Axiom foo : + forall st st' lid, + (AppendEntries lid -> In st) -> AppendEntries lid -> In st'. + +Definition params := prod whatever raft_data. + +Goal forall + (d : raft_data), + (forall (h : name) (w : whatever), + AppendEntries w -> In (@snd whatever raft_data (@nw params h))) -> + In d. +Proof. +intros. +eapply foo. +intros. +solve [debug eauto]. +Abort. + +End Bar. 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. |