aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-11-05Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel fu...Maxime Dénès
2018-11-03Merge PR #8852: Use the obligation evar flagPierre-Marie Pédrot
2018-11-02Merge PR #8834: [error printing] Fix improper grounding of open terms in prin...Hugo Herbelin
2018-10-31Introduce Safe_typing.set_share_reductionMaxime Dénès
2018-10-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-28[error printing] Fix improper grounding of open terms in printing.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 #7186: Moving `fold_constr_with_full_binders` to a placeMaxime Dénès
2018-10-19Merge PR #8758: [api] Qualify access to `Nametab`Hugo Herbelin
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
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-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Merge PR #8589: Correct some spelling errors (continued)Emilio Jesus Gallego Arias
2018-10-15Mini-factorization preparing unification.Hugo Herbelin
2018-10-15Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.Hugo Herbelin
2018-10-15DeclareDef: Reorganizing declaration of definitions in a more structured way.Hugo Herbelin
2018-10-15Merge PR #8716: Lemmas: Little simplification of artificially convoluted codeEmilio Jesus Gallego Arias
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-12Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.Hugo Herbelin
2018-10-12Lemmas: Little simplification of artificially convoluted code.Hugo Herbelin
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-11[vernac] Remove unused `start_hook` `save_hook` from Lemmas.Emilio Jesus Gallego Arias
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-09Simplify code for [Definition := Eval ...]Gaëtan Gilbert
2018-10-07Adding missing header to comFixpoint.ml.Hugo Herbelin
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-06Merge PR #8555: Remove section paths from kernel namesPierre-Marie Pédrot
2018-10-05Using smart mkLambdaCN/mkProdCN.Hugo Herbelin
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-03Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac he...Pierre-Marie Pédrot
2018-10-02Update the -compat flagsJason Gross
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-10-01Merge PR #8501: [classes] Split large `new_instance` function up.Matthieu Sozeau
2018-09-30[api] Cleanup `Decls`: remove unused function, move vernac helper.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 12:16:34 +0000