| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8. |  Maxime Dénès | 2015-06-24 |
| * | Do not display the status of monomorphic constants unless in universe-polymor... |  Guillaume Melquiond | 2015-03-09 |
| * | Adapting output tests to the removal of the new token warning and to |  Hugo Herbelin | 2014-10-21 |
| * | Reductionops: (Co)Fixpoints are always refolded during iota |  Pierre Boutillier | 2014-09-18 |
| * | Fixing output test-suite: since universe polymorphism, the Print command |  Pierre-Marie Pédrot | 2014-05-08 |
| * | Fixing 2 output test-suites. |  ppedrot | 2013-10-08 |
| * | Continuation of r16346 on filtering local definitions. Refined |  herbelin | 2013-03-30 |
| * | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... |  pboutill | 2013-02-25 |
| * | A small test for type inference (used to be a regression at some time). | herbelin | 2011-12-04 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |