| 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. | |||
| 2019-01-22 | Turn `Refine Instance Mode` off by default | Maxime Dénès | |
| 2019-01-08 | Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` ↵ | Maxime Dénès | |
| proofs. We forbid commands that may open proofs inside proofs. | |||
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |