| Age | Commit message (Collapse) | Author |
|
Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.
|
|
|
|
|
|
|
|
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
generalizing * which was broken since 8.4.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
reference manual.
|
|
|
|
|
|
|
|
|
|
Structures. Text mode + a "Require Import" in a module which provokes
suspect warnings "Exception Not_found".
|
|
Set Printing Existential Instances (see bug report #3951).
|
|
match the overall style.
|
|
It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.
|
|
part.
|
|
|
|
|
|
Fixes #3939.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In particular document the "once" behaviour.
|
|
In particular try to avoid the use of the word "backtracking" which refers to too many things.
|
|
|
|
|
|
|
|
Updating my own work and others when I could think of them.
|
|
|
|
|
|
|
|
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|