aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2017-11-27Merge PR #6241: [lib] Generalize Control.timeout type.Maxime Dénès
2017-11-27Merge PR #6041: Protecting the printing of filenames with spaceMaxime Dénès
2017-11-24[lib] Generalize Control.timeout type.Emilio Jesus Gallego Arias
2017-11-24Merge PR #6197: [plugin] Remove LocalityFixme über hack.Maxime Dénès
2017-11-23Quote file names which have spaces in "Print LoadPath".Hugo Herbelin
2017-11-23Merge PR #6203: Fix universe polymorphic Program obligations.Maxime Dénès
2017-11-22[plugin] Remove LocalityFixme über hack.Emilio Jesus Gallego Arias
2017-11-22[plugin] Encapsulate modifiers to vernac commands.Emilio Jesus Gallego Arias
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-22Fix universe polymorphic Program obligations.Matthieu Sozeau
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-21Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Maxime Dénès
2017-11-21Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Maxime Dénès
2017-11-20Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Maxime Dénès
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Maxime Dénès
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
2017-11-19[plugins] Prepare plugin API for functional handling of state.Emilio Jesus Gallego Arias
2017-11-19[vernac] Increase table size.Emilio Jesus Gallego Arias
2017-11-19[proof] Attempt to deprecate some V82 parts of the proof API.Emilio Jesus Gallego Arias
2017-11-16Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Maxime Dénès
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-08Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Hugo Herbelin
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-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-06Merge PR #6063: Finish removing Show Goal uidMaxime Dénès
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
2017-11-01provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesMatej Košík
2017-10-27Merge PR #677: Trunk+abstracting injection flagsMaxime Dénès
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-10-24Removing dead code which raised questions.Hugo Herbelin
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-17[vernac] [state] Cache freeze/unfreezeEmilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-17[stm] Move interpretation state to VernacentriesEmilio Jesus Gallego Arias
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Code factorization Vernacentries.interp on VernacProof.Gaëtan Gilbert
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
2017-10-10Merge PR #1053: [deps] Move `Discharge` to `interp`Maxime Dénès
2017-10-09Merge PR #1114: Generic handling of nameable objects for pluginsMaxime Dénès
2017-10-09[deps] Move `Discharge` to `interp`Emilio Jesus Gallego Arias
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Maxime Dénès
2017-10-06Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...Maxime Dénès
2017-10-05Merge PR #1081: Mini fix at improving the cannot unify error messageMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 07:08:12 +0000