aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Maxime Dénès
2017-10-05Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-10-03Implementing a generic mechanism for locating named objects from Coq side.Pierre-Marie Pédrot
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-25BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsPaul Steckler
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Maxime Dénès
2017-09-25Merge PR #1057: Reporting locations in error messages about notation formats.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:37:41 +0000