| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-06-30 | [declaremods] Remove abstraction of imperative module operations | Emilio Jesus Gallego Arias | |
| Now that `Printmods` is above `Declaremods`, we don't need to pass the extra `mod_ops` argument. | |||
| 2020-06-30 | [states] Move States to vernac | Emilio Jesus Gallego Arias | |
| We continue to push state layers upwards, in preparation of a functional vernacular interpretation. Now we move `States` and `Printmod` which messes with the global state as to temporarily create envs with modules. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |