aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\
| * Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
| * Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| * COMMENTS: PredicateGravatar Matej Kosik2016-01-05
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | Remove some useless module opening.Gravatar Guillaume Melquiond2016-01-02
* | Avoid warnings about loop indices.Gravatar Guillaume Melquiond2016-01-02
* | Fix typos.Gravatar Guillaume Melquiond2016-01-01
* | Remove unused hashconsing code.Gravatar Guillaume Melquiond2016-01-01
* | Do not make it harder on the compiler optimizer by packing arguments.Gravatar Guillaume Melquiond2016-01-01
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\|
* | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
| * Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* | Sharing toplevel representation for several generic types.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | Attaching a dynamic argument to the toplevel type of generic arguments.Gravatar Pierre-Marie Pédrot2015-12-21
* | Trust the directory cache in batch mode.Gravatar Guillaume Melquiond2015-12-21
* | COMMENTS: added to the "Unicode" module.Gravatar Matej Kosik2015-12-18
* | COMMENTS: updated in the "Option" module.Gravatar Matej Kosik2015-12-18
* | COMMENTS: added to the "Predicate" moduleGravatar Matej Kosik2015-12-18
| * spawn: fix leak of file descriptorsGravatar Enrico Tassi2015-12-17
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
* | Adding compatibility flag for 8.5.Gravatar Hugo Herbelin2015-12-14
* | Remove some occurrences of Unix.opendir.Gravatar Guillaume Melquiond2015-12-14
* | Removing dead unsafe code in Genarg.Gravatar Pierre-Marie Pédrot2015-12-12
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removingGravatar Hugo Herbelin2015-12-10
| * Remove remaining occurrences of Unix.readdir.Gravatar Guillaume Melquiond2015-12-09
| * Replace Unix.readdir by Sys.readdir in dir cache.Gravatar Emilio Jesus Gallego Arias2015-12-09
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
* | Leveraging GADTs to provide a better Dyn API.Gravatar Pierre-Marie Pédrot2015-12-05
* | Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
| * Fix for case-insensitive path looking continued (#2554): Adding aGravatar Hugo Herbelin2015-11-25
| * Generalizing the patch to bug #2554 on fixing path looking withGravatar Hugo Herbelin2015-11-25
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Fixed #4274, bad formatting of messages in emacs mode.Gravatar Pierre Courtieu2015-10-19
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-14
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
| * CThread: blocking read + threads now worksGravatar Enrico Tassi2015-10-08
| * Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
| * Future: make not-here/not-ready messages customizableGravatar Enrico Tassi2015-10-08