| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
Was needed to be done for a while.
|
| |
|
|
| |
This is needed to fix `Declare ML Module "ltac_plugin".
|
| |
|
|
| |
This is in preparation for landing of PR#309: Ltac as a plugin
|
| | |
|
| |
|
|
|
|
|
| |
This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.
It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | |
|
| |\ \
| | |
| | |
| | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
| | |
| |
| |
| |
| |
| | |
Reporting location was not expecting a term passed to an ML tactic to
be interpreted by the ML tactic itself. Made an empirical fix to
report about the as-precise-as-possible location available.
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
| |
|
|
|
|
| |
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.
|
| | | |
|
| | |
| |
| |
| | |
Getting closer from before when the bug was introduced + test.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
Changes:
- data structures are purely functional (so retracting do work)
- profiling data flows towards master using the feedback bus
- master aggregates the data on printing
|
| | |
| |
| |
| |
| | |
calls are logged too. Using appropriate printer for reparsability of
the output.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The problem came from the fact that the legacy beta-reduction occurring
after a rewrite was wrongly applied to the side-conditions of the
rewriting step. We restrict it to the correct goal in this patch.
|
| | | |
|
| | |
| |
| |
| |
| | |
This was an overlook. There was no reason to let it in the tactics/ folder,
as is was semantically part of the Ltac implementation.
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| | |
when the rewrite lemma doesn't typecheck or does not
correspond to a relation.
|
| | | |
|
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Enrico Tassi
Matthieu Sozeau
Matthieu Sozeau
Jason Gross
Jason Gross