| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2018-07-25 | Optimized dependencies for pattern-matching on only trivial patterns. | Hugo Herbelin | |
| If a term is matched only against variables, it will not introduce a "match" and thus, even if the term is of an inductive type, its indices will not be taken into account in the current algorithm (though one could imagine an algorithm which does an expansion specially in order to filter on indices). This allows to tell the unification not to use dependencies which the pattern-matching algorithm is not able to exploit in practice. See example in file 2733.v. | |||
| 2013-09-20 | Get rid of "shouldsucceed" subdirectory by moving tests to parent directory. | xclerc | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |