aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
* | CLEANUP: Simplifying the changes done in "kernel/*"Gravatar Matej Kosik2016-02-15
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
|/
* Fix bug when discharging universe constraints coming from variablesGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Small optimization in Cooking: do not construct identity substitutions.Gravatar Pierre-Marie Pédrot2014-08-13
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.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
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
* Noise for nothingGravatar pboutill2012-03-02
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09