| Age | Commit message (Expand) | Author |
|---|
| 2019-07-02 | [declare] Cleanup on imports, move exception. | Emilio Jesus Gallego Arias |
| 2019-07-02 | Merge PR #10336: Improve the ambiguous paths warning to indicate which path ... | Gaëtan Gilbert |
| 2019-07-02 | Merge PR #10340: [vernac] Remove special status of Load, turn it into VtNoProof | Gaëtan Gilbert |
| 2019-07-02 | Improve the ambiguous paths warning to indicate which path is ambiguous with ... | Kazuhiko Sakaguchi |
| 2019-07-01 | Update doc for % escapes in Sphinx doc, improve error messages | Jim Fehrle |
| 2019-07-01 | [declare] Remove superfluous API | Emilio Jesus Gallego Arias |
| 2019-07-01 | [decls] Remove goal_object_kind type. | Emilio Jesus Gallego Arias |
| 2019-07-01 | [api] Reduce declare_kinds even more. | Emilio Jesus Gallego Arias |
| 2019-07-01 | [declare] Separate kinds from entries in constant declaration | Emilio Jesus Gallego Arias |
| 2019-07-01 | [dumpglob] Move dumpglob-specific data to dumpglob. | Emilio Jesus Gallego Arias |
| 2019-07-01 | [api] Refactor most of `Decl_kinds` | Emilio Jesus Gallego Arias |
| 2019-07-01 | [pretyping] Remove seemingly unless check about "variable" opacity. | Emilio Jesus Gallego Arias |
| 2019-07-01 | Merge PR #10433: [vernac] Cleanup on interface of Vernacentries | Gaëtan Gilbert |
| 2019-06-30 | Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG. | Emilio Jesus Gallego Arias |
| 2019-06-28 | Merge PR #10438: Kernel transparent definition entries have no body universes. | Pierre-Marie Pédrot |
| 2019-06-28 | Merge PR #10434: [declare] Fine tuning of Hook type. | Pierre-Marie Pédrot |
| 2019-06-28 | Reify libobject containers | Maxime Dénès |
| 2019-06-27 | Merge PR #10443: Fix dev/doc/README.md by removing redundant, outdated info. | Clément Pit-Claudel |
| 2019-06-27 | Fix dev/doc/README.md by removing redundant, outdated info. | Théo Zimmermann |
| 2019-06-27 | [vernac] Cleanup on interface of Vernacentries | Emilio Jesus Gallego Arias |
| 2019-06-27 | [extraction] Remove not very useful call to dumpglob. | Emilio Jesus Gallego Arias |
| 2019-06-27 | Kernel transparent definition entries have no body universes. | Gaëtan Gilbert |
| 2019-06-27 | Merge PR #10429: Perform the opaque section variable inference outside of the... | Gaëtan Gilbert |
| 2019-06-27 | [vernac] Remove special status of Load, turn it into VtNoProof | Emilio Jesus Gallego Arias |
| 2019-06-27 | Merge PR #10337: [stm] [vernac] Remove special ?proof parameter from vernac m... | Enrico Tassi |
| 2019-06-26 | [ci] Overlays for #10337 | Emilio Jesus Gallego Arias |
| 2019-06-26 | [proof] finalize_proof doesn't need opaque (it's already in entries) | Gaëtan Gilbert |
| 2019-06-26 | Perform the opaque section variable inference outside of the kernel. | Pierre-Marie Pédrot |
| 2019-06-26 | Remove dead code for typing of section definitions in kernel. | Pierre-Marie Pédrot |
| 2019-06-26 | [stm] [vernac] Remove special ?proof parameter from vernac main path | Emilio Jesus Gallego Arias |
| 2019-06-26 | Merge PR #9855: [Fail] Simplify `Fail` implementation. | Gaëtan Gilbert |
| 2019-06-26 | Merge PR #10351: [lemmas] Move `Stack` out of Lemmas. | Gaëtan Gilbert |
| 2019-06-26 | [ci] Overlays for #10434 | Emilio Jesus Gallego Arias |
| 2019-06-26 | [declare] Fine tuning of Hook type. | Emilio Jesus Gallego Arias |
| 2019-06-26 | Merge PR #10401: Fix printers test | Emilio Jesus Gallego Arias |
| 2019-06-26 | Merge PR #10427: Move internal flag | Emilio Jesus Gallego Arias |
| 2019-06-25 | Re-add the "Show Goal" command for Prooftree in PG. | Jim Fehrle |
| 2019-06-25 | Merge PR #10344: Allow to pass Ltac2 values to Ltac1 quotations | Enrico Tassi |
| 2019-06-25 | [lemmas] Move `Stack` out of Lemmas. | Emilio Jesus Gallego Arias |
| 2019-06-25 | Move the internal_flag type from Declare to Ind_tables. | Pierre-Marie Pédrot |
| 2019-06-25 | Remove the internal_flag argument from Declare API. | Pierre-Marie Pédrot |
| 2019-06-25 | Make dependence in Declare explicit in tactics. | Pierre-Marie Pédrot |
| 2019-06-25 | Give a functional type to Ltac1 quotations with a context. | Pierre-Marie Pédrot |
| 2019-06-25 | Documenting the Ltac2 change. | Pierre-Marie Pédrot |
| 2019-06-25 | Adding the ability to transfer Ltac2 variables to Ltac1 quotations. | Pierre-Marie Pédrot |
| 2019-06-25 | Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec t... | Pierre-Marie Pédrot |
| 2019-06-25 | Merge PR #10219: [Ltac2] Add util files for Bool, List, Option | Pierre-Marie Pédrot |
| 2019-06-25 | Merge PR #10162: Fix #10161: occur check when defining an algebraic universe. | Pierre-Marie Pédrot |
| 2019-06-25 | Merge PR #10284: Expose set interface to option tables | Pierre-Marie Pédrot |
| 2019-06-25 | Merge PR #10412: Add output-coqtop test directory that runs output tests with... | Enrico Tassi |
