| Age | Commit message (Collapse) | Author |
|---|
|
window to query pane in text
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Cygwin/Windows
|
|
|
|
|
|
Closes #6509.
|
|
|
|
pane; use color descriptions
|
|
|
|
Should help with
https://github.com/coq/coq/issues/5675#issuecomment-353604702
Also replace a tab with spaces
|
|
|
|
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
|
This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
|
|
|
|
|
|
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This should help with #5675, in particular with
https://github.com/coq/coq/issues/5675#issuecomment-349716292
|
|
|
|
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|
I don't understand what is wrong with putting a query in a script
running in the IDE. It is typically needed when giving demos, and that
sounds like a ligitimate use case. By the way, we do it ourselves every year
during the demo at CoqPL...
|
|
|
|
|
|
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
|
|
|
|
|
|
|
|
|
possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
|
|
|
|
|
|
|
|
|
