| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This change fixes performance problems in PIDE based user interfaces
|
|
|
|
goal in Instance. Also remove some dead code.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Implement wish #3582.
|
|
Fixes bug #2762.
|
|
Fixes bug #4026.
|
|
Only tactics are taken into account.
|
|
|
|
disabled in the kernel.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
|
|
|
|
When setoid rewriting in a hypothesis, we push the newly introduced declaration
after the last declaration it depends on.
|
|
generalizing * which was broken since 8.4.
|
|
|
|
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
|
|
do not contribute. Fixes bug #3808.
|
