| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Most of it seems straightforward.
|
|
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
|
|
|
of List
|
|
|
|
|
|
|
|
Still some discrepancies though. E.g.:
- some functions taking an equality as arguments have suffix `_f` but
not all;
- the functions possibly raising an error have still different kinds
of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange,
and when in the first two cases, with no unique rules in the style
of the associated string - we thus avoid to document the exact
string used).
There are a few semantics changes:
- skipn_at_least now raises a `Failure` if its argument is negative;
- map3 raises an Invalid_argument "List.map3" rather than
Invalid_argument "map3" and similarly for map4
- internally, map3 and map4 are now tail-recursive (by uniformity);
- internally, split3 and combine3 are now tail-recursive (by uniformity);
- filter is now "smart" by default and smartfilter is deprecated;
- smartmap is now tail-recursive by default.
|
|
|
|
|
|
|
|
|
|
Instead of having the projection data in the constant data we have it
independently in the environment.
|
|
Close #7562.
[api] move hint_info ast to tactics.
|
|
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
|
|
|
|
|
|
|
|
|
In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
Should it be removed? The underlying
`universe_subst -> constr -> constr`
seems like it could be useful for plugins but where would the
substitution be from?
|
|
|
|
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.
|
|
- Be more precise when trying to clear an hypothesis which
occurs implicitly in a global constant.
- Warns if destruct/induction cannot clear an hypothesis occurring
implicitly in a global.
In the first case, the change in situation
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a.
is:
- before: "a is used in conclusion"
- after: "a is used implicitly in b in conclusion"
In the second case:
Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a.
produces a warning: "Cannot remove a, it is used implicitly in b".
|
|
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
|
