| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Instead of setting globally the option, we add a hook to set it in
the init object of the plugin.
|
|
|
|
|
|
|
|
This should save a lot of useless reallocations and hashset crawling, which
end up costing a lot.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
`Require`.
|
|
|
|
constructor it is.
|
|
|
|
|
|
|
|
Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css
files in subdirectories of doc/refman/html. These subdirectories cause
a failure when doing [install doc/refman/html/* target].
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
implementation from Detyping.
|
|
|
|
|
|
|
|
|
|
|
|
The fix covers the case of a non-dependent goal with unavailable
dependent case analysis: destruct was not seeing that it could still
use non-dependent case analysis.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This prevents careless confusions with generic arguments from Coq.
|
|
|
|
|
