aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Remove remnants of polymorphic instance name registration.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-11-07Merge PR #8773: [checker] Refactor by sharing code with the kernelPierre-Marie Pédrot
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-11-06[program] extend obligation to give back a mapping from obligations toMatthieu Sozeau
2018-11-05Merge PR #8899: Remove the deprecated Token module and port the corresponding...Emilio Jesus Gallego Arias
2018-11-05Merge PR #8871: [library] Move Nametab/Lib specific-names to NametabHugo Herbelin
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-05Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel fu...Maxime Dénès
2018-11-04Remove the deprecated Token module and port the corresponding code.Pierre-Marie Pédrot
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-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Per command attribute parsing for core commandsGaëtan Gilbert
2018-11-02Load doesn't support attributesGaëtan Gilbert
2018-11-02Simplify use of polymorphism/program globals in attributesGaëtan Gilbert
2018-11-02Remove is_universe_polymorphic in indschemesGaëtan Gilbert
2018-11-02Remove evdref style in build_combined_schemeGaëtan Gilbert
2018-11-02Generalize attributes further to get a monad (mostly for [map])Gaëtan Gilbert
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02Remove pointless optional arguments to mk_attsGaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert
2018-11-02Remove location field from attributesGaëtan Gilbert
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
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-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:31:04 +0000