aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Maxime Dénès
2018-01-20Remove dead code in Environ.Pierre-Marie Pédrot
2018-01-19Fix context handling of fix and cofix in Ltac subterm matching.Cyprien Mangin
2018-01-19Define EConstr version of [push_rec_types].Cyprien Mangin
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-30Using a dedicated type for Lib.abstr_info.Pierre-Marie Pédrot
2017-12-27Remove the local polymorphic flag hack.Maxime Dénès
2017-12-27Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Maxime Dénès
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
2017-12-14Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Maxime Dénès
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Maxime Dénès
2017-12-14Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Maxime Dénès
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12Decompiling pattern-matching: mini-removal dead code.Hugo Herbelin
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-12-12Further clean-up in Reductionops, removing unused lift arguments.Maxime Dénès
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-11Merge PR #6338: Remove up-to-conversion term matchingMaxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-09Remove up-to-conversion matching functions.Pierre-Marie Pédrot
2017-12-06Getting rid of the Update constructor in Reductionops.Pierre-Marie Pédrot
2017-12-06Getting rid of the Shift constructor in Reductionops.Pierre-Marie Pédrot
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Maxime Dénès
2017-11-30Remove unused boolean from cl_context field of Typeclasses.typeclassGaëtan Gilbert
2017-11-28Adding a variant get_truncation_family_of of get_sort_family_of.Hugo Herbelin
2017-11-28Moving non-recursive function sort_family_of out of the retype block of recur...Hugo Herbelin
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:19:33 +0000