| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
| |
|
|
| |
(Universes and Evd)
|
| |
|
|
|
|
|
|
|
|
|
| |
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| | |/
|/| |
|
| | |
| |
| |
| |
| | |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
| |/ /
| |
| |
| |
| |
| |
| |
| | |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When restricting an evar with candidates, raise an exception if this
restriction would leave the evar without candidates, i.e. unsolvable.
- evarutil: mark restricted evars as "cleared"
They would otherwise escape being catched by the [advance] function
of clenv, and result in dangling evars not being registered to the shelf.
- engine: restrict_evar marks it cleared, update the future goals
We make the new evar a future goal and remove the old one.
If we did nothing, [unshelve tac] would work correctly as it
uses [Proofview.advance] to find the shelved goals, going through
the cleared evar. But [Unshelve] would fail as it expects only
undefined evars on the shelf and throws away the defined ones.
|
| |\
| |
| |
| | |
possibility of an "eqn" clause
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This is a quick fix. Code should be made nicer along these lines:
- try to pass the name of the variable created by "mkletin_goal" in
the monad using "refine_one";
- use a disjunctive type of "inhyps" to indicate when it is
meaningful, rather than using [].
|
| | |
| |
| |
| | |
We move the last 3 types to more adequate places.
|
| | |
| |
| |
| |
| | |
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
|
| | |
| |
| |
| |
| | |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | | |
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | | |
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.
|
Siddharth Bhat
Gaëtan Gilbert
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Gaëtan Gilbert
Armaël Guéneau
Enrico Tassi
Maxime Dénès
Matthieu Sozeau
Emilio Jesus Gallego Arias
Théo Zimmermann