aboutsummaryrefslogtreecommitdiff
path: root/vernac/assumptions.ml
AgeCommit message (Expand)Author
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-10-12Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.Hugo Herbelin
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-25Fixing #8532 (regression in Print Assumptions within a functor).Hugo Herbelin
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-05Fixing #8416 (Print Assumptions missing module information from compiled files).Hugo Herbelin
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
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-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 10:27:57 +0000