| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
|
| |
|
|
| |
Fix done with Enrico.
|
| |
|
|
|
|
| |
csdp.cache -> .csdp.cache
lia.cache -> .lia.cache
nlia.cache -> .nia.cache
|
| |
|
|
|
|
|
|
| |
Previously, setting an unknown option was an error or a warning,
depending on the type of the option. We make it always a warning, for
forward compatibility.
This was already fixed in 8.6.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
The logic was backward: if the path of a symbol was a prefix of the
current path, then the current path (without sections) was used. But what
we want is that, if the current path (without sections) is a prefix of the
path of a symbol, then the former should be used.
This fixes about 1,600 broken links in the documentation of the standard
library.
|
| |
|
|
| |
Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
|
| |
|
|
|
| |
Option Standard Proposition Elimination Scheme from 8.5 was not
documented in the right section.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
Moreover, this commit makes sure that an empty line after a list is always
translated into a break. ("StartLevel 1" was excluded, for some reason.)
It also avoids some code duplication. In particular, "stop_item ()" is
defined as "reach_item_level 0", so there is no reason to handle
"StartLevel 1" specially.
|
| |\ |
|
| |/
|
|
|
|
|
|
| |
In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".".
In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed.
I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Modulo delta for types should be fully transparent.
|
| | |
|
| |
|
|
| |
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
|
| | |
|
| | |
|
| |\ |
|
| |/
|
|
|
| |
when checking that the rewrite relation is homogeneous in
setoid_rewrite.
|
| |\ |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
We should really automate the generation of the log of fixes for CHANGES.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
Was PR#243: fixing nsatz
|
| | |
| |
| |
| | |
Note that even "Load Verbose" is not supposed to display them.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The -verbose family of options is only meant to echo sentences as they are
processed. The patch below broke this, while fixing another issue. That
other issue will be fixed in the next commit.
Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its"
This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
we use a hashtable to reduce the complexity of creating
a duplicate-free list.
|
| |\ \
| | |
| | |
| | | |
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#241: Restore option_map in FMapFacts
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
the function in_ideal of ideal.ml supposes the list of polynomials
does not contain zero and is duplicate free.
I force this invariant in the call of in_ideal in nsatz.ml4
the function clean_pol returns the reduced list plus a list of
booleans that indicates which polynomials have been deleted
the function expand_pol translates back the certificate of
the reduced to list to the complete list thanks to the list
of booleans.
The fix is quadratic with respect to the input list which should
be ok for reasonable usage of nsatz.
If there is some performance issue we could improve the in_pol
function.
|
| | | |
| | |
| | | |
This way, it's not eaten by a section
|
Pierre-Marie Pédrot
Maxime Dénès
Frédéric Besson
Hugo Herbelin
Guillaume Melquiond
Enrico Tassi
Xavier Leroy
Matthieu Sozeau
Matthieu Sozeau
thery
Jason Gross
Jason Gross