aboutsummaryrefslogtreecommitdiffhomepage
path: root/clib
Commit message (Collapse)AuthorAge
* Add documentation for Dyn.Gravatar whitequark2018-06-21
|
* Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.Gravatar whitequark2018-06-21
|
* Reformat Dyn.{ml,mli}.Gravatar whitequark2018-06-21
|
* Merge PR #7841: Remove CanaryGravatar Pierre-Marie Pédrot2018-06-19
|\
| * Remove Canary.Gravatar whitequark2018-06-18
| | | | | | | | This eliminates 3 uses of Obj from TCB.
* | Remove Hashcons.Hobj.Gravatar whitequark2018-06-17
|/ | | | This eliminates 12 uses of Obj from TCB.
* cArray: proper invalid_arg exceptionsGravatar Matthieu Sozeau2018-06-15
|
* Merge PR #7406: Fix #7214: install knows which ml files do not get compiled ↵Gravatar Pierre-Marie Pédrot2018-06-11
|\ | | | | | | to cmx.
* | [lib] Fix wrong deprecation comment.Gravatar Emilio Jesus Gallego Arias2018-06-10
| |
* | Further sharing in CList.Gravatar Hugo Herbelin2018-06-03
| |
* | Cleaning, documentation, uniformisation of the Coq extension of List.Gravatar Hugo Herbelin2018-06-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Still some discrepancies though. E.g.: - some functions taking an equality as arguments have suffix `_f` but not all; - the functions possibly raising an error have still different kinds of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange, and when in the first two cases, with no unique rules in the style of the associated string - we thus avoid to document the exact string used). There are a few semantics changes: - skipn_at_least now raises a `Failure` if its argument is negative; - map3 raises an Invalid_argument "List.map3" rather than Invalid_argument "map3" and similarly for map4 - internally, map3 and map4 are now tail-recursive (by uniformity); - internally, split3 and combine3 are now tail-recursive (by uniformity); - filter is now "smart" by default and smartfilter is deprecated; - smartmap is now tail-recursive by default.
* | [lib] Fix wrong deprecation annotations.Gravatar Emilio Jesus Gallego Arias2018-06-03
| | | | | | | | Introduced in #7177
* | Collecting Map.smart_* functions into a module Map.Smart.Gravatar Hugo Herbelin2018-05-23
| |
* | Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| |
* | Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| |
* | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
| |
* | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| |
* | Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.Gravatar Hugo Herbelin2018-05-23
| | | | | | | | This follows the model of smartmap and smartmap2.
* | CArray: adding combinators.Gravatar Hugo Herbelin2018-05-23
| |
| * Remove unused Deque filesGravatar Gaëtan Gilbert2018-05-02
|/
* Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\
* | Adding Array.fold_left4.Gravatar Hugo Herbelin2018-03-28
| |
| * [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|/
* Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified.
* Add function bind in option.ml.Gravatar Hugo Herbelin2018-03-08
|
* Tweak comments to fix ocamldoc errorsGravatar mrmr19932018-03-05
|
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* When printing a notation with "match", more flexibility in matching equations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | We reason up to order, and accept to match a final catch-all clauses with any other clause. This allows for instance to parse and print a notation of the form "if t is S n then p else q".
* In printing notations with "match", reasoning up to the order of clauses.Gravatar Hugo Herbelin2018-02-20
|
* Adding skewed lists.Gravatar Pierre-Marie Pédrot2017-12-29
| | | | | This is a purely functional datastructure isomorphic to usual lists, except that it features a O(log n) lookup while preserving the O(1) cons operation.
* [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Emilio Jesus Gallego Arias2017-12-23
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.