| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-24 | Remove the indirect opaque accessor hooks from Opaqueproof. | Pierre-Marie Pédrot | |
| We simply pass them as arguments, now that they are not called by the kernel anymore. The checker definitely needs to access the opaque proofs. In order not to touch the API at all, I added a hook there, but it could also be provided as an additional argument, at the cost of changing all the upwards callers. | |||
| 2019-01-08 | Add 'doc/plugin_tutorial/' from commit ↵ | Gaëtan Gilbert | |
| '168a13dab1c9987f592994150997e692d4d7e40b' git-subtree-dir: doc/plugin_tutorial git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7 git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |