aboutsummaryrefslogtreecommitdiff
path: root/kernel/term_typing.mli
AgeCommit message (Expand)Author
2019-05-20Do not perform the section variable check on global recipes.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-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-10-19Explicitly merge contexts in side-effect universe handling.Pierre-Marie Pédrot
2018-10-19Move side-effect typing into Safe_env.Pierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
2017-07-26Statically ensuring that inlined entries out of the kernel have no effects.Pierre-Marie Pédrot
2017-07-26Further simplication: do not recreate entries for side-effects.Pierre-Marie Pédrot
2017-07-26More precise type of entries capturing their lack of side-effects.Pierre-Marie Pédrot
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-23Documenting the API of side-effects.Pierre-Marie Pédrot
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
2017-01-20Do not add redundant side effects in tactic code.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-01-20Update copyright headers.Maxime Dénès
2015-10-29Cleanup API and comments of 908dcd613Enrico Tassi
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-09-25Add a field in `constant_body` to track constant whose well-foundedness is as...Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-08-08State Transaction Machinegareuselesinge
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-02-27Minor cleanup around Term_typingletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-08-08Updating headers.herbelin
2011-12-12Proof using ...gareuselesinge
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:41:30 +0000