diff options
| author | Matthieu Sozeau | 2016-10-21 18:16:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-21 18:16:16 +0200 |
| commit | 517cc63a18d95c02c2d2490adb110ff712d30375 (patch) | |
| tree | 22c6e527663803ceec47afc625bb1a2e5b75adad /test-suite/bugs | |
| parent | cef86ed6f78e2efa703bd8772a43fbeba597bbe3 (diff) | |
| parent | 5609da1e08f950fab85b87b257ed343b491f1ef5 (diff) | |
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/4763.v | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5097.v | 7 |
2 files changed, 7 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v deleted file mode 100644 index ae8ed0e6e8..0000000000 --- a/test-suite/bugs/closed/4763.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. -Coercion is_true : bool >-> Sortclass. -Global Instance: Transitive leb. -Admitted. - -Goal forall x y z, leb x y -> leb y z -> True. - intros ??? H H'. - lazymatch goal with - | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] - => pose proof (transitivity H H' : is_true (R x z)) - end. - exact I. -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 0000000000..37b239cf61 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,7 @@ +(* Tracing existing evars along the weakening rule ("clear") *) +Goal forall y, exists x, x=0->x=y. +intros. +eexists ?[x]. +intros. +let x:=constr:(ltac:(clear y; exact 0)) in idtac x. +Abort. |