| Age | Commit message (Expand) | Author |
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès |
| 2017-09-15 | Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon... | Maxime Dénès |
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert |
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot |
| 2017-08-31 | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès |
| 2017-08-31 | Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate | Maxime Dénès |
| 2017-08-31 | Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag | Maxime Dénès |
| 2017-08-31 | Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ... | Maxime Dénès |
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès |
| 2017-08-29 | Merge PR #946: Functional pretyping interface | Maxime Dénès |
| 2017-08-29 | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map | Hugo Herbelin |
| 2017-08-25 | primproj: fix bug 5245, hnf on proj with simpl never flag. | Matthieu Sozeau |
| 2017-08-24 | Program: fix BZ#5683, missing lift when building case predicate | Matthieu Sozeau |
| 2017-08-22 | use OCaml 4.03-compatible Filename functions | Paul Steckler |
| 2017-08-22 | Prevent overallocation in Array.map_to_list and remove custom implementation ... | Guillaume Melquiond |
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler |
| 2017-08-18 | move filename search to start_profiler | Paul Steckler |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès |
| 2017-08-01 | Remove understand_tcc_evars. | Maxime Dénès |
| 2017-08-01 | Move type_uconstr to Tacinterp. | Maxime Dénès |
| 2017-08-01 | Remove understand_judgment and understand_judgment_tcc. | Maxime Dénès |
| 2017-08-01 | Remove allow_anonymous_refs. | Maxime Dénès |
| 2017-08-01 | Remove pure_open_constr (now open_constr) | Maxime Dénès |
| 2017-08-01 | Move glob_constr_ltac_closure to evar_refiner. | Maxime Dénès |
| 2017-08-01 | Merge PR #913: Less allocations in Detyping | Maxime Dénès |
| 2017-08-01 | Merge PR #806: closing bug 5315 | Maxime Dénès |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès |
| 2017-07-29 | closing bug 5315 | Julien Forest |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík |
| 2017-07-26 | Add a comment regarding the specialization of the combinator in Detyping. | Pierre-Marie Pédrot |
| 2017-07-26 | Removing template polymorphism for definitions. | Pierre-Marie Pédrot |
| 2017-07-21 | Allocation-friendly detyping of term arrays. | Pierre-Marie Pédrot |
| 2017-07-20 | Merge branch 'v8.7' | Maxime Dénès |
| 2017-07-13 | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot |
| 2017-07-13 | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Discharge. | Pierre-Marie Pédrot |
| 2017-07-13 | Make the typeclass implementation fully compatible with universe polymorphism. | Pierre-Marie Pédrot |
| 2017-07-13 | Safer API for Global.type_of_global_in_context. | Pierre-Marie Pédrot |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Recordops. | Pierre-Marie Pédrot |
| 2017-07-13 | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel | Maxime Dénès |
| 2017-07-11 | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann |
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot |
| 2017-07-11 | Less footguns in universe handling: remove subst_instance_context. | Pierre-Marie Pédrot |
| 2017-07-11 | Getting rid of simple calls to AUContext.instance. | Pierre-Marie Pédrot |
| 2017-07-07 | Merge PR #863: Fixing environment in warning "Projection value has no head co... | Maxime Dénès |
| 2017-07-07 | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-28 | A fix for #5598 (no discharge of Existing Classes referring to local variables). | Hugo Herbelin |