diff options
| author | letouzey | 2013-09-19 17:37:23 +0000 |
|---|---|---|
| committer | letouzey | 2013-09-19 17:37:23 +0000 |
| commit | ea4180b729f90630941b5501ef83f94b6c8ecd6b (patch) | |
| tree | 52ea7518691912771255aaf386712bb8324d8c61 /kernel/type_errors.ml | |
| parent | efae3184752f19a6cfb95b05ad42438c87ee3a9e (diff) | |
universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes
This file, which is currently expected to fail at the last line
(with Universe Inconsistency), was actually failing earlier
after Pierre Boutillier changed the patterns (parameters are required now).
A final "Fail" will soon arrives here to avoid such issue in the future...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions