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