aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
Commit message (Expand)AuthorAge
* 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
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of identifierGravatar ppedrot2012-12-14
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
* Environ.set_universes is dead codeGravatar letouzey2011-10-26
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Environ: generic equality on named_context replaced by named_context_equalGravatar puech2011-07-29