aboutsummaryrefslogtreecommitdiff
path: root/clib
AgeCommit message (Expand)Author
2018-10-18[clib] Provide `filter_range` function.Emilio Jesus Gallego Arias
2018-10-16Merge PR #8738: [clib] Deprecate string functions available in OCaml 4.05Pierre-Marie Pédrot
2018-10-16[clib] Remove Array functions available in OCaml 4.05.0Emilio Jesus Gallego Arias
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
2018-10-13Add unicode category LMMirai IKEBUCHI
2018-10-07Merge PR #8493: [api] Remove (most) 8.9 deprecated objects.Pierre-Marie Pédrot
2018-10-06Merge PR #7850: Rewrite CEphemeron to use a type-safe implementation based on...Pierre-Marie Pédrot
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-04Merge PR #8626: [ocaml] [lib] Remove some compatibility layers for OCaml < 4....Pierre-Marie Pédrot
2018-10-03Rename CEphemeron.clear→clean for clarity.whitequark
2018-10-03Rewrite CEphemeron to use a type-safe implementation based on GADTs.whitequark
2018-10-03[pretyper] Remove imperative passing of evar_map.Emilio Jesus Gallego Arias
2018-10-02[ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0Emilio Jesus Gallego Arias
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-03[doc] Build ML API documentation artifact.Emilio Jesus Gallego Arias
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-23Generate more compact escape sequences byJim
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
2018-06-21Add documentation for Dyn.whitequark
2018-06-21Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.whitequark
2018-06-21Reformat Dyn.{ml,mli}.whitequark
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-18Remove Canary.whitequark
2018-06-17Remove Hashcons.Hobj.whitequark
2018-06-15cArray: proper invalid_arg exceptionsMatthieu Sozeau
2018-06-11Merge PR #7406: Fix #7214: install knows which ml files do not get compiled t...Pierre-Marie Pédrot
2018-06-10[lib] Fix wrong deprecation comment.Emilio Jesus Gallego Arias
2018-06-03Further sharing in CList.Hugo Herbelin
2018-06-03Cleaning, documentation, uniformisation of the Coq extension of List.Hugo Herbelin
2018-06-03[lib] Fix wrong deprecation annotations.Emilio Jesus Gallego Arias
2018-05-23Collecting Map.smart_* functions into a module Map.Smart.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-23Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.Hugo Herbelin
2018-05-23CArray: adding combinators.Hugo Herbelin
2018-05-02Remove unused Deque filesGaëtan Gilbert
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-03-28Adding Array.fold_left4.Hugo Herbelin
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-08Add function bind in option.ml.Hugo Herbelin
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20When printing a notation with "match", more flexibility in matching equations.Hugo Herbelin
2018-02-20In printing notations with "match", reasoning up to the order of clauses.Hugo Herbelin