aboutsummaryrefslogtreecommitdiff
path: root/kernel/cooking.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with Co...Maxime Dénès
2019-05-26Actually merge Discharge into Cooking.Pierre-Marie Pédrot
2019-05-25Centralize the hashconsing of constant declarations.Pierre-Marie Pédrot
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-07-03Cooking.cook_constant: remove unused env argument.Gaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Using a record type for Cooking.result.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-03-27Fix hashconsing of terms in the kernel.Pierre-Marie Pédrot
2016-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-02-27Minor cleanup around Term_typingletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-18Proof using: nested sections bugfixgareuselesinge
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:00:27 +0000