aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Maxime Dénès
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-22[api] A few more minor deprecation notices.Emilio Jesus Gallego Arias
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo...Maxime Dénès
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaëtan Gilbert
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6117: Fix printing anomaly in convMaxime Dénès
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-08Fixing 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-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-05Refining 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-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...Maxime Dénès
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph...Maxime Dénès
2017-10-28Fixing #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-17unification: fix BZ#5692, recognize prim projs as CS projectionsMatthieu Sozeau
2017-10-17Properly handling projection parameters in canonical structures.Pierre-Marie Pédrot
2017-10-17Handling primitive projections in canonical structures.Pierre-Marie Pédrot
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...Maxime Dénès
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-09-28Remove trivial TODO comment (constants can't be template poly now).Gaëtan Gilbert
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...Maxime Dénès
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Maxime Dénès
2017-09-23After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Hugo Herbelin
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
2017-09-22Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...Maxime Dénès
2017-09-21Proposing meta names more distinguishable from evar names than ?M42.Hugo Herbelin
2017-09-21A 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-19Merge PR #1036: Unify EConstr.t equalityMaxime Dénès
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Maxime Dénès
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-09-08Using EConstr equality check in unification.Pierre-Marie Pédrot
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:42:45 +0000