| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-20 | Remove VtUnknown classification | Maxime Dénès | |
| This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638. | |||
| 2018-10-04 | test-suite: cleaning | Vincent Laporte | |
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |