| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
| |
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
| |
|
|
|
|
| |
Importing VectorNotations breaks `; []`. So we make sure it's not
imported by defualt. Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
|
|
|
Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
|
Théo Zimmermann
Jason Gross