| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Find a more efficient fix for dealing with template universes: |  Matthieu Sozeau | 2014-05-06 |
| * | Try a new way of handling template universe levels | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Propagating conversion_problem towards (postponed) evar/evar problems. |  Hugo Herbelin | 2014-04-01 |
| * | Removing useless array-to-list and converse casts used in |  ppedrot | 2013-10-22 |
| * | Continuation of r16346 on filtering local definitions. Refined |  herbelin | 2013-03-30 |
| * | Repairing r16205: errors raised by check_evar_instance were no longer | herbelin | 2013-02-28 |
| * | Added propagation of evars unification failure reasons for better | herbelin | 2013-02-17 |
| * | Splitted Evarutil in two files | ppedrot | 2013-02-10 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |