aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
Commit message (Expand)AuthorAge
* Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\
| * Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
| * Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* | Assertion checking that invariant enforced by 0f8d1b92 always holds.Gravatar Maxime Dénès2015-09-10
|/
* Fixing pop_rel_context.Gravatar Hugo Herbelin2015-08-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Cleaner interfaces for linking locations of native compiler.Gravatar Maxime Dénès2014-11-12
* Fix retroknowledge for int31 division.Gravatar Maxime Dénès2014-10-24
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Make the retroknowledge marshalable.Gravatar Arnaud Spiwack2014-09-24
* 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
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* - 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
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Int31 decompilation in native compiler was still partial. Now fixed.Gravatar Maxime Dénès2014-04-09
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
* Full support for int31 values in native compiler.Gravatar Maxime Dénès2014-04-09
* Partial support for open terms in int31.Gravatar Maxime Dénès2014-04-09
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
* Environ: export API to transitively close a set of section variablesGravatar Enrico Tassi2014-01-05
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
* Revert "Fast lookup_named in environments, based on maps instead of lists."Gravatar ppedrot2013-11-15
* Fast lookup_named in environments, based on maps instead of lists.Gravatar ppedrot2013-11-13
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* Safe_typing code refactoringGravatar letouzey2013-08-20
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 09:02:25 +0000