| Age | Commit message (Collapse) | Author |
|---|
|
points of Camlp5
|
|
Z into three files
|
|
Fixes #7857.
|
|
|
|
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
|
|
|
|
|
|
|
|
constants
|
|
|
|
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
|
|
|
|
|
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
|
This is a first step towards the acceptance of mutual record types in the
kernel.
|
|
|
|
- we always rename
- we compile {clear}/view to /view{clear}
|
|
|
|
|
|
We only use it locally, so we simply register the ML tactic inside the module
but we do not export the syntax.
|
|
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.
|
