| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| |\| | | | | | | |
|
| | | |_|_|/ / /
| |/| | | | | |
|
| | |\ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#321: Handling of section variables in hints
|
| | | | | | | | | |
|
| | |\ \ \ \ \ \ \ |
|
| | | |\ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was PR#338: Remove warning now that info_auto is fixed.
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Removes a warning dating from 8.5 signaling that info_auto
and info_trivial are broken and advising to use Info 1 auto
instead. Now, these tactics are fixed and thus they can be
used again. They do not do exactly the same thing as
Info 1 auto and may be more useful for the learner.
|
| | | |_|_|/ / / / /
| |/| | | | | | | |
|
| | | |/ / / / / /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6.
This behavior of refine has changed three times in recent years, so
let's take the time to make up our mind and wait for a major release.
Btw, onhyps=None is not a sane way to express that a tactic should be
applied to all hypotheses.
|
| | | |_|/ / / /
| |/| | | | | |
|
| | | | | | | | |
|
| | | |_|/ / /
| |/| | | |
| | | | | |
| | | | | |
| | | | | | |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| | | |/ / /
| |/| | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
| |\| | | | |
|
| | |\| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
"msg_debug (mt())" is not identity, so we return back to how it was
done in 8.4, contracting a repeated pattern-matching into one.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Header was missing in last commit.
One day, it would be nice to unify the display of "debug auto" and
"debug eauto"...
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
There was a catch-all clause in the tclORELSE0 function. We now only
catch noncritical exceptions.
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is more precise and probably clearer (see e.g. thread
"Understanding auto" on coq-club).
|
| |\| | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.
See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
|
| |\| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |\| | | | |
|
| | | | | | |
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#263: Fast lookup in named contexts
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
between proofs in tactic injection, with a side-effect on inversion.
|
| |\| | | | | |
|
| | |\ \ \ \ \
| | | |/ / /
| | |/| | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
This does not affect the semantics of these functions.
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| | |\| | | | |
|
| | | |\ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#293: Fix #4762 (eauto weaker than auto).
|
| | | | | | | | |
|
| | | |_|_|_|/
| |/| | | |
| | | | | |
| | | | | | |
unresolvable
|
| | | |/ / / |
|
| |\| | | | |
|
| | |\| | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
the case for clear and the conversion tactics.
|
| |\| | | | |
|
Matthieu Sozeau
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Théo Zimmermann
Arnaud Spiwack
Yves Bertot
Théo Zimmermann
Cyprien Mangin