diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1900.v | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1901.v | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1977.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1981.v | 5 |
4 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/shouldsucceed/1900.v new file mode 100644 index 0000000000..cf03efda42 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1900.v @@ -0,0 +1,8 @@ +Parameter A : Type . + +Definition eq_A := @eq A. + +Goal forall x, eq_A x x. +intros. +reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v new file mode 100644 index 0000000000..598db36601 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1901.v @@ -0,0 +1,11 @@ +Require Import Relations. + +Record Poset{A:Type}(Le : relation A) : Type := + Build_Poset + { + Le_refl : forall x : A, Le x x; + Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; + Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. + +Definition nat_Poset : Poset Peano.le. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/shouldsucceed/1977.v new file mode 100644 index 0000000000..28715040ce --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1977.v @@ -0,0 +1,4 @@ +Inductive T {A} : Prop := c : A -> T. +Goal (@T nat). +apply c. exact 0. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v new file mode 100644 index 0000000000..0c3b96dad9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1981.v @@ -0,0 +1,5 @@ +Implicit Arguments ex_intro [A]. + +Goal exists n : nat, True. + eapply ex_intro. exact 0. exact I. +Qed. |