aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
Commit message (Expand)AuthorAge
* Cooking.cook_constant: remove unused env argument.Gravatar Gaëtan Gilbert2018-07-03
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Merge PR #7715: Simplify the cooking of primitive projections.Gravatar Maxime Dénès2018-06-23
|\
* | Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| * Simplify the cooking of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-11
|/
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Add a comment about universe lifting in sections in the kernel.Gravatar Pierre-Marie Pédrot2017-12-31
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* Hardening universe abstraction in Cooking.Gravatar Pierre-Marie Pédrot2017-12-30
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
* Asserting that monomorphic section variables have no abstracted context.Gravatar Pierre-Marie Pédrot2017-07-11
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Fix hashconsing of terms in the kernel.Gravatar Pierre-Marie Pédrot2017-03-27
* CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 04:34:52 +0000