| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-21 | Fixing typos - Part 1 | JPR | |
| 2019-02-12 | [tactics] Remove dependency of abstract on global proof state. | Emilio Jesus Gallego Arias | |
| In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary. | |||
| 2018-12-13 | [engine] Allow debug printers to access the environment. | Emilio Jesus Gallego Arias | |
| This should improve correctness and will be needed for the PRs that remove global access to the proof state. | |||
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-20 | proofview: goals come with a state | Enrico Tassi | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent of Logic. | Pierre-Marie Pédrot | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond | |
| Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. | |||
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-28 | Moving Proofview_monad to the engine/ folder. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |