aboutsummaryrefslogtreecommitdiff
path: root/kernel/pre_env.ml
AgeCommit message (Expand)Author
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-20COMMENT: Pre_env.envMatej Kosik
2017-04-20simplifying "Environ.push_named" functionMatej Kosik
2017-04-10Revert "simplify: Environ.push_named"Matej Košík
2017-04-10simplify: Environ.push_namedMatej Kosik
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2017-01-17Mapping named_context_val preserves sharing when possible.Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-09Removing the now useless field env_named_val from named_context_val.Pierre-Marie Pédrot
2016-09-09More efficient implementation of map_named_val.Pierre-Marie Pédrot
2016-09-09Tentative fast-access named envPierre-Marie Pédrot
2016-09-09Packing the named_context_val in a proper record and marking it private.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-05-16Revert "Decent error message when a constant is not found"Enrico Tassi
2014-05-16Decent error message when a constant is not foundEnrico Tassi
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-06Inductive maps in Environ now use HMap.Pierre-Marie Pédrot
2014-03-05Using HMaps in Safe_env.environments, hopefully improving performances.Pierre-Marie Pédrot
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
2014-01-06STM: fix worker crash when doing vm_computeEnrico Tassi
2013-12-29Got rid of unused lazy flag in the native compiler.Maxime Dénès
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
2013-11-15Revert "Fast lookup_named in environments, based on maps instead of lists."ppedrot
2013-11-13Fast lookup_named in environments, based on maps instead of lists.ppedrot
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-29Allocation-friendly version of [Pre_env.push_named].ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2012-12-14Modulification of identifierppedrot
2012-11-13More monomorphizationsppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:54:11 +0000