| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-12 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-12 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-16 | Adding variants enter_one and refine_one which assume that exactly one | Hugo Herbelin | |
| goal is under focus and which support returning a relevant output. | |||
| 2016-06-16 | Proofview: extensions for backtracking eauto | Matthieu Sozeau | |
| unshelve_goals is used to correctly register dependent subgoals that have to be solved. Resolution may fail to do so using hints, so we have to put them back as goals in that case. The shelf is a good interface for doing that. unifiable can be used outside proofview to detect dependencies between goals. This might be better in another module. | |||
| 2016-06-16 | Implement limited proof search and iterative deepening. | Matthieu Sozeau | |
| Fix typo in proofview | |||
| 2016-06-16 | Merge 'pr/191' into trunk | Enrico Tassi | |
| 2016-06-14 | Fix a typo in proofs/proofview.mli. | Cyprien Mangin | |
| 2016-06-14 | Add goal range selectors. | Cyprien Mangin | |
| You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5. | |||
| 2016-06-06 | STM: proof block detection for bullets and { block } | Enrico Tassi | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |