aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2018-10-30Reduction functions based on CClosure should take an envMaxime Dénès
2018-10-30Avoid redefining reduction functions in fun_indMaxime Dénès
2018-10-30Distinguish globalization and pretyping error on unbound variableMaxime Dénès
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-29Fix for bug #8848Matthieu Sozeau
2018-10-29Merge PR #8667: [RFC] Vendoring of Camlp5Pierre-Marie Pédrot
2018-10-29Merge PR #8780: Cleanup comparing projections through their constants.Maxime Dénès
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-29[camlp5] Fix warnings, switch Coq to vendored library.Emilio Jesus Gallego Arias
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-26Merge PR #8684: Remove a few circumvolutions around parameters of inductive e...Gaëtan Gilbert
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-10-26Merge PR #8707: Separate cache representation between CClosure and CBVMaxime Dénès
2018-10-20Cleanup comparing projections through their constants.Gaëtan Gilbert
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-17Merge PR #8694: Various cleanups of universe apisPierre-Marie Pédrot
2018-10-16Merge PR #8059: Simplify code for [Definition := Eval ...]Matthieu Sozeau
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-10-14Parameterizing default inhabitant for impossible cases with an environment.Hugo Herbelin
2018-10-14Removing a call to Global.env in evarsolve.Hugo Herbelin
2018-10-11The cbv reduction does not rely on the kernel info data structure anymore.Pierre-Marie Pédrot
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-10Merge PR #6218: Fix #5197, handling of algebraic universesPierre-Marie Pédrot
2018-10-09Fix nativenorm when an evar is in the wrong place.Gaëtan Gilbert
2018-10-08Merge PR #8654: Remove FCast from CClosure.fterm.Maxime Dénès
2018-10-08Fix #5197, handling of algebraic universesMatthieu Sozeau
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Remove FCast from CClosure.fterm.Pierre-Marie Pédrot
2018-10-04Merge PR #7361: Towards selecting "best" unification failure among severalPierre-Marie Pédrot
2018-10-04Merge PR #8581: [pretyper] Remove imperative passing of evar_map.Pierre-Marie Pédrot
2018-10-03Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac he...Pierre-Marie Pédrot
2018-10-03[pretyper] Remove imperative passing of evar_map.Emilio Jesus Gallego Arias
2018-10-03[pretyper] Less imperative passing of the evar_map, part II.Emilio Jesus Gallego Arias
2018-10-03[pretyper] Less imperative passing of the evar_map, part I.Emilio Jesus Gallego Arias
2018-10-03Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the com...Théo Zimmermann
2018-10-02Update the -compat flagsJason Gross
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-30[api] Cleanup `Decls`: remove unused function, move vernac helper.Emilio Jesus Gallego Arias
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-09-27Possible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2018-09-27Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2018-09-27Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 16:36:07 +0000