aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
| |/ / / /
* | | | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
* | | | | Merge PR #1036: Unify EConstr.t equalityGravatar Maxime Dénès2017-09-19
|\ \ \ \ \ | |/ / / / |/| | | |
| | * | | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| |/ / / |/| | |
* | | | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \ \ \
* \ \ \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \
* \ \ \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \
| | | * | | | Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |_|/ / / / |/| | | | |
| | | * | | Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
| |_|/ / / |/| | | |
| | * | | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |/ / / |/| | |
* | | | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* | | | Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\ \ \ \
* \ \ \ \ Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateGravatar Maxime Dénès2017-08-31
|\ \ \ \ \
* \ \ \ \ \ Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagGravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ...Gravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \ \