index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
clib
Age
Commit message (
Expand
)
Author
2018-10-18
[clib] Provide `filter_range` function.
Emilio Jesus Gallego Arias
2018-10-16
Merge PR #8738: [clib] Deprecate string functions available in OCaml 4.05
Pierre-Marie Pédrot
2018-10-16
[clib] Remove Array functions available in OCaml 4.05.0
Emilio Jesus Gallego Arias
2018-10-16
[clib] Deprecate string functions available in OCaml 4.05
Emilio Jesus Gallego Arias
2018-10-13
Add unicode category LM
Mirai IKEBUCHI
2018-10-07
Merge PR #8493: [api] Remove (most) 8.9 deprecated objects.
Pierre-Marie Pédrot
2018-10-06
Merge 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-04
Merge PR #8626: [ocaml] [lib] Remove some compatibility layers for OCaml < 4....
Pierre-Marie Pédrot
2018-10-03
Rename CEphemeron.clear→clean for clarity.
whitequark
2018-10-03
Rewrite 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.0
Emilio 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-27
Add support for focusing on named goals using brackets.
Théo Zimmermann
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-07-23
Displays the differences between successive proof steps in coqtop and CoqIDE.
Jim Fehrle
2018-07-23
Generate more compact escape sequences by
Jim
2018-06-25
Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...
Matthieu Sozeau
2018-06-22
Define and use UGraph.enforce_leq_alg for subtyping inference
Gaëtan Gilbert
2018-06-21
Add documentation for Dyn.
whitequark
2018-06-21
Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.
whitequark
2018-06-21
Reformat Dyn.{ml,mli}.
whitequark
2018-06-19
Merge PR #7841: Remove Canary
Pierre-Marie Pédrot
2018-06-18
Remove Canary.
whitequark
2018-06-17
Remove Hashcons.Hobj.
whitequark
2018-06-15
cArray: proper invalid_arg exceptions
Matthieu Sozeau
2018-06-11
Merge 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-03
Further sharing in CList.
Hugo Herbelin
2018-06-03
Cleaning, documentation, uniformisation of the Coq extension of List.
Hugo Herbelin
2018-06-03
[lib] Fix wrong deprecation annotations.
Emilio Jesus Gallego Arias
2018-05-23
Collecting Map.smart_* functions into a module Map.Smart.
Hugo Herbelin
2018-05-23
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.
Hugo Herbelin
2018-05-23
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.
Hugo Herbelin
2018-05-23
CArray: adding combinators.
Hugo Herbelin
2018-05-02
Remove unused Deque files
Gaëtan Gilbert
2018-04-12
Merge PR #6972: [api] Deprecate a couple of aliases that we missed.
Maxime Dénès
2018-03-28
Adding Array.fold_left4.
Hugo Herbelin
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-09
Delayed weak constraints for cumulative inductive types.
Gaëtan Gilbert
2018-03-08
Add function bind in option.ml.
Hugo Herbelin
2018-03-05
Tweak comments to fix ocamldoc errors
mrmr1993
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-20
When printing a notation with "match", more flexibility in matching equations.
Hugo Herbelin
2018-02-20
In printing notations with "match", reasoning up to the order of clauses.
Hugo Herbelin
[prev]
[next]