| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
| |
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| |
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
| | |
|
|
|
This makes sense here as the main client is `Stdargs`. This helps with
the concerns @herbelin had in
https://github.com/coq/coq/issues/6008#issuecomment-341107793
|
Emilio Jesus Gallego Arias
Théo Zimmermann