| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2014-06-26 | Change interface of refresh universes to get a pbty argument instead of | Matthieu Sozeau | |
| the computed direction argument. In case pbty is conv, no refreshing is done as the evar body must be convertible with the given term, however refreshing of template application evar arguments can still happen. (Re)-Closing bug #2966. | |||
| 2013-01-28 | Fixed bug #2966 (de Bruijn error in computation of heads for coercions). | herbelin | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |