diff options
author | 2016-10-08 17:41:15 +0200 | |
---|---|---|
committer | 2016-10-08 17:41:15 +0200 | |
commit | 1a9fe0dfe837ccbee25e9ecf19a7b2e7768a7958 (patch) | |
tree | d0539f4fe40c2a3077858c6c69440d98de053964 /test-suite | |
parent | 2dcd8f2e82366bb3b0f51a42426ccdfbb00281dc (diff) | |
parent | 82eb6cbfa3db53756ea40fb4795836d6f8c55bbe (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/4464.v | 4 | ||||
-rw-r--r-- | test-suite/bugs/closed/4529.v | 45 | ||||
-rw-r--r-- | test-suite/bugs/closed/4763.v | 13 | ||||
-rw-r--r-- | test-suite/bugs/closed/5066.v | 7 |
4 files changed, 69 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v new file mode 100644 index 000000000..f8e9405d9 --- /dev/null +++ b/test-suite/bugs/closed/4464.v @@ -0,0 +1,4 @@ +Goal True -> True. +Proof. + intro H'. + let H := H' in destruct H; try destruct H. diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v new file mode 100644 index 000000000..8b3c24fec --- /dev/null +++ b/test-suite/bugs/closed/4529.v @@ -0,0 +1,45 @@ +(* File reduced by coq-bug-finder from original input, then from 1334 lines to 1518 lines, then from 849 lines to 59 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 22 2016 18:20:47 with OCaml 4.02.3 + coqtop version r-schnelltop:/home/r/src/coq/coq,(HEAD detached at V8.5) (5e23fb90b39dfa014ae5c4fb46eb713cca09dbff) *) +Require Coq.Setoids.Setoid. +Import Coq.Setoids.Setoid. + +Class Equiv A := equiv: relation A. +Infix "≡" := equiv (at level 70, no associativity). +Notation "(≡)" := equiv (only parsing). + +(* If I remove this line, everything compiles. *) +Set Primitive Projections. + +Class Dist A := dist : nat -> relation A. +Notation "x ={ n }= y" := (dist n x y) + (at level 70, n at next level, format "x ={ n }= y"). + +Record CofeMixin A `{Equiv A, Dist A} := { + mixin_equiv_dist x y : x ≡ y <-> forall n, x ={n}= y; + mixin_dist_equivalence n : Equivalence (dist n); +}. + +Structure cofeT := CofeT { + cofe_car :> Type; + cofe_equiv : Equiv cofe_car; + cofe_dist : Dist cofe_car; + cofe_mixin : CofeMixin cofe_car +}. +Existing Instances cofe_equiv cofe_dist. +Arguments cofe_car : simpl never. + +Section cofe_mixin. + Context {A : cofeT}. + Implicit Types x y : A. + Lemma equiv_dist x y : x ≡ y <-> forall n, x ={n}= y. +Admitted. +End cofe_mixin. + Context {A : cofeT}. + Global Instance cofe_equivalence : Equivalence ((≡) : relation A). + Proof. + split. + * + intros x. +apply equiv_dist. + diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v new file mode 100644 index 000000000..ae8ed0e6e --- /dev/null +++ b/test-suite/bugs/closed/4763.v @@ -0,0 +1,13 @@ +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/5066.v b/test-suite/bugs/closed/5066.v new file mode 100644 index 000000000..eed7f0f3f --- /dev/null +++ b/test-suite/bugs/closed/5066.v @@ -0,0 +1,7 @@ +Require Import Vector. + +Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) := + match v1 with + | nil _ => v2 + | cons _ e n' sv => vector_rev sv (cons A e n2 v2) + end. |