aboutsummaryrefslogtreecommitdiff
path: root/kernel/pre_env.ml
AgeCommit message (Expand)Author
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
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-03-14Ajout des alias de module dans le noyau.soubiran
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-03-27Modification de la vm:notin
2006-05-12correction bugs de condition de garde (fix + cofix)barras
2005-12-06j'avais oublie ces deux fichiers.gregoire
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:29:16 +0000