aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\
* \ Merge PR #6666: Fix reduction of primitive projections on coinductive records...Gravatar Maxime Dénès2018-01-30
|\ \
| * | [cbv] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
* | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
|/ /
* | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Gravatar Maxime Dénès2018-01-23
|\ \
| * | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
* | | Fix context handling of fix and cofix in Ltac subterm matching.Gravatar Cyprien Mangin2018-01-19
* | | Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
|/ /
| * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
* | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
* | Using a dedicated type for Lib.abstr_info.Gravatar Pierre-Marie Pédrot2017-12-30
|/
* Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
* Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Gravatar Maxime Dénès2017-12-27
|\
* \ Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Gravatar Maxime Dénès2017-12-27
|\ \
| | * [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |/ |/|
* | 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
|\ \
| | * Remove unused boolean from cl_context field of Typeclasses.typeclassGravatar Gaëtan Gilbert2017-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