aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Getting rid of the Update constructor in Reductionops.Gravatar Pierre-Marie Pédrot2017-12-06
* Getting rid of the Shift constructor in Reductionops.Gravatar Pierre-Marie Pédrot2017-12-06
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Gravatar Maxime Dénès2017-11-30
|\
| * Adding a variant get_truncation_family_of of get_sort_family_of.Gravatar Hugo Herbelin2017-11-28
| * Moving non-recursive function sort_family_of out of the retype block of recur...Gravatar Hugo Herbelin2017-11-28
* | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \
* | | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| |/ |/|
| * Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
| * Use Maps and ids for universe bindersGravatar Gaëtan Gilbert2017-11-24
|/
* Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Gravatar Maxime Dénès2017-11-24
|\
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
* | [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/
* Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo...Gravatar Maxime Dénès2017-11-20
|\
| * Fix #5761: cbv on undefined evars under binders produces unbound relGravatar Gaëtan Gilbert2017-11-15
* | [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
* \ Merge PR #6117: Fix printing anomaly in convGravatar Maxime Dénès2017-11-13
|\ \
* \ \ Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Gravatar Maxime Dénès2017-11-13
|\ \ \
* \ \ \ Merge PR #922: New beta-iota compatibility refinementsGravatar Maxime Dénès2017-11-08
|\ \ \ \
| | | * | Fixing missing separator in an error message.Gravatar Hugo Herbelin2017-11-08
| |_|/ / |/| | |
| | | * [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | |/
| | * [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| |/ |/|
* | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Gravatar Maxime Dénès2017-11-06
|\ \
* | | Refining PR#924 (insensitivity of projection heuristics to alphabet).Gravatar Hugo Herbelin2017-11-05
| * | [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
|/ /
* | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...Gravatar Maxime Dénès2017-11-03
|\ \
* \ \ Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph...Gravatar Maxime Dénès2017-11-03
|\ \ \
| | * | Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
| |/ / |/| |
* | | [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* | | unification: fix BZ#5692, recognize prim projs as CS projectionsGravatar Matthieu Sozeau2017-10-17
* | | Properly handling projection parameters in canonical structures.Gravatar Pierre-Marie Pédrot2017-10-17
* | | Handling primitive projections in canonical structures.Gravatar Pierre-Marie Pédrot2017-10-17
* | | Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\ \ \
* \ \ \ Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...Gravatar Maxime Dénès2017-10-03
|\ \ \ \
| | * | | Remove some duplication between Typeops and Nativenorm.Gravatar Gaëtan Gilbert2017-09-29
| | * | | Remove trivial TODO comment (constants can't be template poly now).Gravatar Gaëtan Gilbert2017-09-28
* | | | | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
* | | | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| |/ / / |/| | |
* | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \ \ \
* \ \ \ \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \
| | | | * | | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Gravatar Hugo Herbelin2017-09-23
| |_|_|/ / / |/| | | | |
| * | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | * | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |/ / / / |/| | | |
* | | | | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \
| * | | | | Proposing meta names more distinguishable from evar names than ?M42.Gravatar Hugo Herbelin2017-09-21
| * | | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| |/ / / /