| Age | Commit message (Collapse) | Author |
|---|
|
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
|
Also renaming fold_map' into fold_right_map, and fold_map2' into
fold_right2_map.
|
|
[kind_of_term].
To be able to write equality up to evar instantiation instantiation.
Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
|
|
- Optimize the removal of generalization when there is no dependency in
the generalized variable (see postprocess_dependencies, and the removal
of dependencies in the default type of impossible cases).
- Compute the onlydflt flag correctly (what allows automatic treatment
of impossible cases even when there is no clause at all).
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
Anyway, a few syntactic features of 3.12 were already used here and
there (e.g. local opening via Foo.(...), or the record shortcut
{ field; ... }). Hence compiling with 3.11 wasn't working anymore.
Already take advantage of the following 3.12.1 features :
- "module type of ..." in CArray, CList, CString ...
- "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
via our coqdep to localize the .ml4 modules :-)
The -ml-synonym option (+ various bugfixes) is the reason for asking
3.12.1 directly and not just 3.12.0. After all, if debian stable is
providing 3.12.1, then everybody has it ;-)
|
|
1. Only apply last Zupdates
2. Better smartmap with state.
|
|
higher-order functions like map and iter, and they are modified so that
they take one additional argument, thus saving a cloure allocation.
Compare the following.
Array.iter: ('a -> unit) -> 'a array -> unit
Array.Fun1.iter: ('r -> 'a -> unit) -> 'r -> 'a array -> unit
Basically, Array.Fun1.iter f x v = Array.iter (f x) v, though it does not
allocate a closure.
For now only the most critical functions are recoded.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16910 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
