diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/3593.v (renamed from test-suite/bugs/opened/3593.v) | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4190.v | 15 | ||||
-rw-r--r-- | test-suite/bugs/closed/4191.v | 5 | ||||
-rw-r--r-- | test-suite/bugs/closed/4193.v | 7 | ||||
-rw-r--r-- | test-suite/bugs/closed/4198.v | 13 | ||||
-rw-r--r-- | test-suite/bugs/closed/4214.v | 5 | ||||
-rw-r--r-- | test-suite/bugs/closed/4217.v | 6 |
7 files changed, 52 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/closed/3593.v index d83b90060..378db6857 100644 --- a/test-suite/bugs/opened/3593.v +++ b/test-suite/bugs/closed/3593.v @@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }. Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. simpl; intros. constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). - Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). reflexivity. Qed. diff --git a/test-suite/bugs/closed/4190.v b/test-suite/bugs/closed/4190.v new file mode 100644 index 000000000..2843488ba --- /dev/null +++ b/test-suite/bugs/closed/4190.v @@ -0,0 +1,15 @@ +Module Type A . + Tactic Notation "bar" := idtac "ITSME". +End A. + +Module Type B. + Tactic Notation "foo" := fail "NOTME". +End B. + +Module Type C := A <+ B. + +Module Type F (Import M : C). + +Lemma foo : True. +Proof. +bar. diff --git a/test-suite/bugs/closed/4191.v b/test-suite/bugs/closed/4191.v new file mode 100644 index 000000000..290bb384d --- /dev/null +++ b/test-suite/bugs/closed/4191.v @@ -0,0 +1,5 @@ +(* Test maximal implicit arguments in the presence of let-ins *) +Definition foo (x := 1) {y : nat} (H : y = y) : True := I. +Definition bar {y : nat} (x := 1) (H : y = y) : True := I. +Check bar (eq_refl 1). +Check foo (eq_refl 1). diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v new file mode 100644 index 000000000..885d04a92 --- /dev/null +++ b/test-suite/bugs/closed/4193.v @@ -0,0 +1,7 @@ +Module Type E. +End E. + +Module Type A (M : E). +End A. + +Fail Module Type F (Import X : A). diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v new file mode 100644 index 000000000..ef991365d --- /dev/null +++ b/test-suite/bugs/closed/4198.v @@ -0,0 +1,13 @@ +Require Import List. +Open Scope list_scope. +Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), + let k := + (match H in (_ = y) return x = hd x y with + | eq_refl => eq_refl + end : x = x') + in k = k. + simpl. + intros. + match goal with + | [ |- appcontext G[@hd] ] => idtac + end. diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v new file mode 100644 index 000000000..cd53c898e --- /dev/null +++ b/test-suite/bugs/closed/4214.v @@ -0,0 +1,5 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +reflexivity. diff --git a/test-suite/bugs/closed/4217.v b/test-suite/bugs/closed/4217.v new file mode 100644 index 000000000..19973f30a --- /dev/null +++ b/test-suite/bugs/closed/4217.v @@ -0,0 +1,6 @@ +(* Checking correct index of implicit by pos in fixpoints *) + +Fixpoint ith_default + {default_A : nat} + {As : list nat} + {struct As} : Set. |