aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_054.v
Commit message (Collapse)AuthorAge
* remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
|
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
* Fix semantics of change p with c to typecheck c at each specific occurrence ↵Gravatar Matthieu Sozeau2014-06-23
| | | | | | | of p, avoiding unwanted universe constraints in presence of universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113.
* Update various polyproj bugs w.r.t. latest trunkGravatar Jason Gross2014-05-12
|
* Move opened bugs to bugs/openedGravatar Jason Gross2014-05-10
|
* Add more regression tests for univ poly/prim projGravatar Jason Gross2014-05-10
hese regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently fails. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one.