| Age | Commit message (Expand) | Author |
|---|
| 2017-11-20 | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo... | Maxime Dénès |
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert |
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias |
| 2017-11-13 | Merge PR #6098: [api] Move structures deprecated in the API to the core. | Maxime Dénès |
| 2017-11-13 | Merge PR #6117: Fix printing anomaly in conv | Maxime Dénès |
| 2017-11-13 | Merge PR #6065: [api] Deprecate all legacy uses of Names in core. | Maxime Dénès |
| 2017-11-08 | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès |
| 2017-11-08 | Fixing missing separator in an error message. | Hugo Herbelin |
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias |
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias |
| 2017-11-06 | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès |
| 2017-11-05 | Refining PR#924 (insensitivity of projection heuristics to alphabet). | Hugo Herbelin |
| 2017-11-04 | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias |
| 2017-11-03 | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia... | Maxime Dénès |
| 2017-11-03 | Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph... | Maxime Dénès |
| 2017-10-28 | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin |
| 2017-10-25 | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias |
| 2017-10-17 | unification: fix BZ#5692, recognize prim projs as CS projections | Matthieu Sozeau |
| 2017-10-17 | Properly handling projection parameters in canonical structures. | Pierre-Marie Pédrot |
| 2017-10-17 | Handling primitive projections in canonical structures. | Pierre-Marie Pédrot |
| 2017-10-09 | Merge PR #1109: Handle some misc todos | Maxime Dénès |
| 2017-10-03 | Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42... | Maxime Dénès |
| 2017-09-29 | Remove some duplication between Typeops and Nativenorm. | Gaëtan Gilbert |
| 2017-09-28 | Remove trivial TODO comment (constants can't be template poly now). | Gaëtan Gilbert |
| 2017-09-28 | Efficient computation of the names contained in an environment. | Pierre-Marie Pédrot |
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot |
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès |
| 2017-09-25 | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ... | Maxime Dénès |
| 2017-09-25 | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4... | Maxime Dénès |
| 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 |
