| Age | Commit message (Expand) | Author |
|---|
| 2017-09-23 | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly. | Hugo Herbelin |
| 2017-09-23 | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791). | Hugo Herbelin |
| 2017-09-23 | Fixing _rect bug for inductive types with let-ins and non-rec uniform params. | Hugo Herbelin |
| 2017-09-22 | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex... | Maxime Dénès |
| 2017-09-21 | Proposing meta names more distinguishable from evar names than ?M42. | Hugo Herbelin |
| 2017-09-21 | A possible fix to BZ#5750 (ability to print context of ltac subterm match). | Hugo Herbelin |
| 2017-09-20 | [flags] Flag `open Flags` | Emilio Jesus Gallego Arias |
| 2017-09-19 | Merge PR #1036: Unify EConstr.t equality | Maxime Dénès |
| 2017-09-19 | Allow declaring universe constraints at definition level. | Matthieu Sozeau |
| 2017-09-15 | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already. | Maxime Dénès |
| 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-12 | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond |
| 2017-09-08 | Using EConstr equality check in unification. | Pierre-Marie Pédrot |
| 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-21 | Fixing another regression with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin |
| 2017-08-21 | Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps. | Hugo Herbelin |
| 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 | Fixing one part of #5669 (unification heuristics sensitive to choice of names). | Hugo Herbelin |
| 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 |
