| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
This way, files importing Core don't have to keep track of the list of runtime operations, for unfoling.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
multiple files
|
|\ |
|
| | |
|
| | |
|
| |
| |
| |
| | |
Now it lines up with the things in Z.Definitions
|
| | |
|
| |
| |
| |
| |
| | |
This required admitting some proofs. @jadephilipoom, please
sanity-check this.
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
arguments since more context variables were used in the definitions than in the placeholder axioms
|
| |
|
| |
|
| |
|
|
|
|
| |
Partial work towards #218
|
|
|
|
|
| |
Note that this makes the axiom we added false. It has a very long and
descriptive name to account for this fact.
|
| |
|
|
|
|
| |
Not sure if locally adding hypotheses is the best way to do it.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
eval_conditional_sub proven
|
| |
|
|
|
|
| |
See [bug #5444](https://coq.inria.fr/bugs/show_bug.cgi?id=5444).
|