aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
Commit message (Expand)AuthorAge
...
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Rename ill-named "imports" field of safe_env into "required".Gravatar Maxime Dénès2015-01-06
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Gravatar Pierre-Marie Pédrot2014-05-11
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Fix universe handling (bug introduced in vi2vo commit)Gravatar Enrico Tassi2014-04-08
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Fix (3243): univ constraints of module subtyping were not propagatedGravatar Enrico Tassi2014-03-11
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
* STM: when batch compiling a vo, assert we behave conservativelyGravatar Enrico Tassi2014-02-26
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Remove obsolete comment about Let being processed synchronouslyGravatar Enrico Tassi2014-01-04
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
* STM: capture type checking error (Closes: 3195)Gravatar Enrico Tassi2013-12-24
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* A shallow copy of a pre_env does not contain the vm cacheGravatar gareuselesinge2013-10-03
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* Remove Obj.magic from safe typingGravatar gareuselesinge2013-08-30
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Safe_typing: minor factorisationGravatar letouzey2013-07-17
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
* Safe_library : a record type for compiled_library instead of large tupleGravatar letouzey2013-03-28
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 05:35:57 +0000