| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |/
|/|
| |
| |
| |
| | |
The code was wrong as it relies once again on term equality and fails
on polymorphic constants. Quote is bound to disappear, so we write a
correct version of this 10-line function in setoid_ring.
|
| |/
|
|
|
|
|
|
|
| |
I think the bug was introduces when apply_type was made safe.
In the test joint to #7255 rewrite (setoid case) generates an
ill-typed goal and apply_type raises a Pretype_error.
It is unclear to me why the tactic monad does not turn the
pretype_error into a UserError
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
| |/
|
|
|
|
| |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
| |
|
|
|
| |
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
| |
|
|
| |
We move the last 3 types to more adequate places.
|
| |
|
|
|
| |
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 add .mli files, removed dead code and use standard combinators
instead of redefined ad-hoc ones in a few places.
A lot of cleaning still has to be done on this code: documenting the
interfaces, resolving the many abstraction leaks. I suspect there is
still a lot of code duplication.
|
| |
|
|
|
| |
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.
We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
| | | |
| | |
| | |
| | |
| | | |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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 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.
|
Pierre-Marie Pédrot
Enrico Tassi
Gaëtan Gilbert
Maxime Dénès
Cyprien Mangin
Emilio Jesus Gallego Arias
Hugo Herbelin
Matthieu Sozeau
Armaël Guéneau
Assia Mahboubi