| Commit message (Collapse) | Author | Age |
... | |
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| |
| |
| |
| |
| |
| | |
The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
|
| |
| |
| |
| |
| | |
For now we only normalize sorts, and we leave instances for the next
commit.
|
|\ \ |
|
| |\| |
|
| | |\
| | | |
| | | |
| | | | |
correctly as…
|
|\| | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
The underlying hint mode implementation was not using the evar-insensitive
API so that it resulted in strange bugs.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Now they are useless because all of the primitives are (should?) be
evar-insensitive.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#172: alternate path separators in typeclass debug output.
|
| |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Before this fix, unshelve typeclasses eauto would produce sub-goals
in the reverse order compared to when they were first shelved.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
A file in the test-suite had to be modified.
It was supposed to reproduce a behavior in intuistionistic-nuprl
but it did not really.
This commit is not supposed to break intuistionistic-nuprl.
|
|/| | | |
| |/ / / |
|
| | | |
| | | |
| | | |
| | | | |
Hit by OCaml's "if then else" with no "end" once more
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We stop failing automatically on non-declared-class nested or toplevel
subgoals as in 8.5, instead of the previous a477dc behavior of shelving
those goals and failing if shelved goals remained at the end of
resolution. It means typeclass resolution during refinement is closer to
all:typeclasses eauto. Hints in typeclass_instances for non-declared
classes can be used during resolution of _nested_ subgoals when it is
fired from type-inference, toplevel goals considered in this case are
still only classes (as in 8.5 and before). The code that triggers the
restriction to only declared class subgoals is commented.
Revert changes to test-suite, adding test for #5203, #5198 is fixed too.
Add corresponding tests in the test-suite (that will break if we,
e.g. disallow non-class subgoals) and update the refman accordingly.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.
Fix test-suite now that shelved goals are allowed
|
| |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| |\ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
|
| | | | | | | |
|