diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 13:54:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 13:54:16 +0200 |
| commit | 0b78edbafedf87f150840228f7d3b7938c809c14 (patch) | |
| tree | abc07c4c71a7d04b2b4634bb6e20b2c75cd74794 /test-suite/bugs/opened | |
| parent | 2fceedc145a0842ec4fa81f488615ea75ac9a29d (diff) | |
Duplicate
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/3385.v | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test-suite/bugs/opened/3385.v b/test-suite/bugs/opened/3385.v deleted file mode 100644 index b4da9cf67..000000000 --- a/test-suite/bugs/opened/3385.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Primitive Projections. -Set Implicit Arguments. -Set Universe Polymorphism. - -Record category := { ob : Type }. - -Goal forall C, ob C -> ob C. -intros C X. - -let y := (eval compute in (ob C)) in constr_eq y (ob C). (* success *) -let y := (eval compute in (@ob C)) in constr_eq y (ob C). (* success *) -(* should be [Fail let y := (eval compute in (@ob C)) in constr_eq y (@ob C).] (really [let y := (eval compute in (@ob C)) in constr_eq y (@ob C)] should succeed, but so long as the [Fail] succeeds, this bug is open), but "not equal" escapes [Fail]. *) -try (let y := (eval compute in (@ob C)) in constr_eq y (@ob C); fail 1). (* failure *) -try (constr_eq (@ob C) (ob C); fail 1). (* failure *) -let y := constr:(@ob C) in -match y with - | ?f C => idtac -end. (* success *) -try (let y := constr:(@ob C) in -match eval compute in y with - | ?f C => idtac -end; fail 1). (* failure: no matching clauses for match *) |