| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \ |
|
| |/ /
|/| |
| | |
| | |
| | | |
In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.
|
| | |
| | |
| | |
| | |
| | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
|\ \ \
| |/ /
|/| | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
| |/
|/| |
|
|\ \
| | |
| | | |
Simplify the newring hack
|
|\ \ \ |
|
| |_|/
|/| |
| | |
| | | |
We address the easy ones, but they should probably be all removed.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
|\ \ \
| | | |
| | | |
| | | | |
in CArray
|
| | | | |
|
| | | | |
|
| | | | |
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | | |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
| | |
| | |
| | |
| | |
| | |
| | | |
The new implementation is 100% compatible with the previous one, but it
is more compact and does not use a tricky translation function from the
kernel.
|
| |/
|/| |
|
|\ \ |
|
| |/
|/| |
|
|\ \ |
|
| | | |
|
| | |
| | |
| | |
| | | |
Uses internal to Refiner remain.
|
| | | |
|
| | | |
|
| |/
|/|
| |
| | |
clear_hyps remain with no alternative
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
| |/ /
|/| |
| | |
| | |
| | |
| | | |
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
|
|\ \ \ |
|
| |/ /
|/| |
| | |
| | | |
Normalization sounds like it should be semantically noop.
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | | |
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | | |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
contains evars
|
| |/ / /
|/| | |
| | | |
| | | |
| | | | |
We take into account all future ipats, not just the ones in
the current branch
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
failure in other file
|
| |_|/ / / /
|/| | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This mitigates bug #6860.
|
| | | | | | |
|
| |_|_|_|/
|/| | | | |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|