| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
~True.
Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.
New behavior deactivated when version is <= 8.5.
|
| |
|
|
| |
Getting closer from before when the bug was introduced + test.
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This way par:eauto and all:eato print the same debugging traecs
|
| | |
| |
| |
| |
| |
| | |
I think that a better place for the mutex would be the printing routine,
but I still hope we will get rid of threads in favor of coroutines.
So I keep all mutexes in Stm.
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip
numbers of seconds and to strip percentages. (This can potentially be
extended later.)
Add a test-suite file to make sure that LtacProf outputs some table.
|
| | | |
| | |
| | |
| | | |
Previously, newlines were missing if a node had no children.
|
| | | |
| | |
| | |
| | | |
This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.)
|
| | | |
| | |
| | |
| | |
| | | |
This required improving the machinery of the test-suite Makefile to
support -compile.
|
| | | |
| | |
| | |
| | | |
not exist.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This legacy function is still used by destruct, and is a hotspot in various
examples from the wild. We hijack the check from Typeclass and perform a
double check at once not to mark unresolvable evars in vain a lot.
|
| | | | |
|
| | | | |
|
| |\ \ \
| |/ /
|/| /
| |/ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
The greatest danger of OCaml's polymorphic equality is that PMP can
replace it with pointer equality at any time, be warned :)
The lack of optimization may account for an exponential blow-up in size
of the generated code, as well as worse runtime performance.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When Mltop.add_rec_path was called to add paths to the loadpath, it was
also adding the top directory to the mlpath. In particular, "theories" was
added to the mlpath although it was explicitly marked "~with_ml:false".
The "plugins" and "user-contribs" subdirectories were scanned twice, once
for filling the loadpath and then for filling the mlpath.
This patch adds an argument to Mltop.add_rec_path to explicitly control
which paths from the loadpath are added to the mlpath (none, the top one,
all of them). The "top" option was the single old behavior; the "none"
option is used for "theories"; the "all" option is used to avoid
duplicate scanning for "plugins" and "user-contribs".
|
| | |
| |
| |
| | |
This was making the test-suite fail on machines where csdp was not installed.
|
| | |
| |
| |
| |
| |
| | |
The previous commit did not apply the beta reduction for compatibility on the
correct goal. We rather apply it on the first generated subgoal. This fixes the
ergo contrib.
|
| | |
| |
| |
| | |
esprit d'escalier : is now also fixed for R
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The number of path canonizations was quadratic in the number of potential
plugin directories. This patch makes it linear; on a standard Coq tree,
this brings the number of chdir and getcwd system calls from more than
1,000 down to about 200 at startup.
This also fixes a bug where the Cd vernacular command could cause plugins
to break since relative paths were used to locate them.
|
| | |
| |
| |
| |
| | |
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
|
| |\ \ |
|
| |/ / |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
There was an "optimization", since Abort is an empty side effect.
But that optimization had an impact on the DAG shape.
Now a nested proof, no matter if it is kept or dropped, is handled the same.
|
Hugo Herbelin
Pierre-Marie Pédrot
Enrico Tassi
Matthieu Sozeau
Jason Gross
Jason Gross
Guillaume Melquiond
Paul Steckler
Maxime Dénès
Frédéric Besson