aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Merge PR #6436: Fix #5368: Canonical structure unification fails.Gravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \
| | * Fix #5368: Canonical structure unification fails.Gravatar Pierre-Marie Pédrot2017-12-15
| |/ |/|
* | Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Gravatar Maxime Dénès2017-12-14
|\ \ \
* \ \ \ Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Gravatar Maxime Dénès2017-12-14
|\ \ \ \
* \ \ \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
| | | | | | * [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
| | | | * | | Decompiling pattern-matching: mini-removal dead code.Gravatar Hugo Herbelin2017-12-12
| | | | * | | In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
| | | | * | | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
| | | * | | | Further clean-up in Reductionops, removing unused lift arguments.Gravatar Maxime Dénès2017-12-12
| | | | |_|/ | | | |/| |
* | | / | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|/ / / |/| | | |
| | * | | Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| |/ / / |/| | |
* | | | Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
* \ \ \ \ Merge PR #6338: Remove up-to-conversion term matchingGravatar Maxime Dénès2017-12-11
|\ \ \ \ \ | |_|_|/ / |/| | | |
| | * | | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |/ / / |/| | |
| | * | [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| |/ / |/| |
| * | Remove up-to-conversion matching functions.Gravatar Pierre-Marie Pédrot2017-12-09
* | | 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
|/ /
| * [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
* | 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
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 21:16:36 +0000