| Age | Commit message (Collapse) | Author |
|---|
|
messages.
|
|
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
|
|
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.
|
|
We simply reuse the same exception as the pretyper instead of raising the
generic failure exception in Tactics.unify.
|
|
(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.
|
