| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92.
|
| |
|
| |
|
|
|
|
| |
The removed code isn't used locally and isn't exported in the signature
|
| |
|
| |
|
|
|
|
|
|
|
| |
Two changes:
- 'a Lazy.t becomes unit -> 'a
- 'a t becomes 'a u (the view type)
This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial.
|
|
|
| |
Lazy.lazy_from_val does almost the same thing as this Obj.magic. It makes some extra dynamic check, but it's frankly unlikely that it could be observed.
|
|
|
| |
View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7
|