aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
* \ Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Maxime Dénès2017-11-21
|\ \
* \ \ Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\ \ \
* \ \ \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Gravatar Maxime Dénès2017-11-20
|\ \ \ \
| | | | * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|_|/ |/| | |
| | * | [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | * | [vernac] Increase table size.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ / |/| |
| | * [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/|
* | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Gravatar Maxime Dénès2017-11-16
|\ \
* | | Fixes #6129 (declaration of coercions made compatible with local definitions).Gravatar Hugo Herbelin2017-11-14
| * | [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
| * | [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|/ /
| * Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Gravatar Hugo Herbelin2017-11-08
* | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* | [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/
* Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Gravatar Maxime Dénès2017-11-06
|\
* \ Merge PR #6063: Finish removing Show Goal uidGravatar Maxime Dénès2017-11-06
|\ \
| | * [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| * | Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
| |/
* / provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesGravatar Matej Košík2017-11-01
|/
* Merge PR #677: Trunk+abstracting injection flagsGravatar Maxime Dénès2017-10-27
|\
| * Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* | Removing dead code which raised questions.Gravatar Hugo Herbelin2017-10-24
|/
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Gravatar Maxime Dénès2017-10-20
|\
* | [vernac] [state] Cache freeze/unfreezeGravatar Emilio Jesus Gallego Arias2017-10-17
* | [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* | [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
* | Parse [Proof using Type] without translating Type to an id.Gravatar Gaëtan Gilbert2017-10-10
* | Use a nice printer for constant names in Suggest Proof Using.Gravatar Gaëtan Gilbert2017-10-10
* | Code factorization Vernacentries.interp on VernacProof.Gravatar Gaëtan Gilbert2017-10-10
* | [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
* | Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
* | Merge PR #1053: [deps] Move `Discharge` to `interp`Gravatar Maxime Dénès2017-10-10
|\ \
* \ \ Merge PR #1114: Generic handling of nameable objects for pluginsGravatar Maxime Dénès2017-10-09
|\ \ \
| | * | [deps] Move `Discharge` to `interp`Gravatar Emilio Jesus Gallego Arias2017-10-09
* | | | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Gravatar Maxime Dénès2017-10-09
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...Gravatar Maxime Dénès2017-10-06
|\ \ \ \
* \ \ \ \ Merge PR #1081: Mini fix at improving the cannot unify error messageGravatar Maxime Dénès2017-10-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \
| | | * | | | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Gravatar Hugo Herbelin2017-10-05
| | | | | | * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
| | | | |_|/ | | | |/| |
| | | | | * Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
| |_|_|_|/ |/| | | |
* | | | | Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\ \ \ \ \
* | | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |_|_|/ / |/| | | |
| * | | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/ / / /
* | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \ \ \
| | | | * BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsGravatar Paul Steckler2017-09-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:27:07 +0000