| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
| |\| | |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
|
| |\| | |
|
| | | | |
|
| | |\ \ |
|
| | | |/
| | |
| | |
| | |
| | |
| | | |
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
| | |/
| |
| |
| |
| | |
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
| | |\
| | |
| | |
| | | |
Was PR#232: Fix the parsing of goal selectors.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
It seems we have no grammar rule that parses floats, so I'm
parsing an integer, but the whole machinery supports floats.
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
| |\ \ \
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.
The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Getting closer from before when the bug was introduced + test.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
This removes a dependency on wit_tactic in Constrintern.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
We also move the Ltac-specific grammar to its folder.
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Previously, newlines were missing if a node had no children.
|
| | | | |
| | | |
| | | |
| | | | |
This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.)
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The previous commit did not apply the beta reduction for compatibility on the
correct goal. We rather apply it on the first generated subgoal. This fixes the
ergo contrib.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | | |
|
| | | | | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Jason Gross
Enrico Tassi
Maxime Dénès
Jason Gross