| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This happens when recursive notations are used to define recursive
notations.
|
| | | |/| | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The move to systematically trying small inversion first bumps
sometimes as feared to the weakness of unification (see #5107).
----
Revert "Posssible abstractions over goal variables when inferring match return clause."
This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94.
Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given."
This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548.
Revert "Trying a no-inversion no-dependency heuristic for match return clause."
This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
|
| | | |/ / /
| | | | |
| | | | |
| | | | |
| | | | | |
side_effects. Partial solution to the handling of side effects
in proofview.
|
| | | |/ / |
|
| |\| | | |
|
| | |\| | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
|
| |\| | | |
|
| | |\| | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
between proofs in tactic injection, with a side-effect on inversion.
|
| | | | | |
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This bug was introduced by 37ab45726, because the new apply_type function
was not checking that the new goal was indeed well-typed. We add this check
locally in the generalize dependent tactic.
|
| | | | |
| | | |
| | | |
| | | | |
Order of items made stable
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#303: LtacProf cutoff is for total percent, not time
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| | |\ \ \ \ \
| | | |_|/ /
| | |/| | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
Restore subst output test file modified by mistake.
|
| | |\ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#302: Set the default LtacProf cutoff to 2%
|
| | | | | | | | |
|
| | | | | | | | |
|
| | |\ \ \ \ \ \
| | | |/ / / /
| | |/| | | | |
|
| | | |\ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#293: Fix #4762 (eauto weaker than auto).
|
| | | | | | | | | |
|
| | | |_|_|_|/ /
| |/| | | | | |
|
| | | |_|/ / /
| |/| | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This was the original value from Tobias' code. When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information. When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want. If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
It seems warnings are not taken into account in output/
tests.
|
| | |\ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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).
|
| | |\ \ \ \ \ |
|
| | | | | | | | |
|
| | | |_|_|_|/
| |/| | | | |
|
| | | | | |/ |
|
| | | | | | |
|
| | | |/ /
| |/| | |
|
| | |/ /
| | |
| | |
| | |
| | |
| | | |
This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
| | | | |
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#232: Fix the parsing of goal selectors.
|
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Maxime Dénès
Pierre-Marie Pédrot
Yves Bertot
Enrico Tassi
Cyprien Mangin
Jason Gross