| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The rationale for its use comes from OCaml weak maps, and is justified by the
fact that Weak.get may prevent its return value to be collected by the GC during
the next slice even though nobody points to it. In our case, this is vastly
irrelevant because hashconsed values are not expected to be collected whatsoever
(save for exceptional cases). But Weak.get_copy is rather costly actually, at
least strictly more than the plain Weak.get.
Experimentally, I observe diminution of compilation time and even diminution
of memory consumption (!) after this patch, so I assume it is a net gain.
|
|
|
|
|
|
|
|
|
|
| |
one_inductive_body so that when eta-expanding at "match" printing time
we know if a let is part of the expected signature or part of the
body.
This is an easy fix for bugs like #3293. Another fix could be to
enforce, as an invariant, or better syntactically, that
"match"/"Case"'s have the body of their branches expanded.
|
| |
|
|
|
|
|
|
| |
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
writing our own comparison functions, and enforcing monomorphization
in many places. This should be more efficient, btw. Still a work
in progress.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
not disrupt anything...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7
|