| Age | Commit message (Expand) | Author |
|---|
| 2019-07-02 | [declare] Cleanup on imports, move exception. | Emilio Jesus Gallego Arias |
| 2019-07-02 | Merge PR #10340: [vernac] Remove special status of Load, turn it into VtNoProof | Gaëtan Gilbert |
| 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 | [api] Refactor most of `Decl_kinds` | Emilio Jesus Gallego Arias |
| 2019-07-01 | Merge PR #10433: [vernac] Cleanup on interface of Vernacentries | Gaëtan Gilbert |
| 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 | [vernac] Cleanup on interface of Vernacentries | Emilio Jesus Gallego Arias |
| 2019-06-27 | [vernac] Remove special status of Load, turn it into VtNoProof | 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 | [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 | [declare] Fine tuning of Hook type. | Emilio Jesus Gallego Arias |
| 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 | Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec t... | Pierre-Marie Pédrot |
| 2019-06-25 | Merge PR #10284: Expose set interface to option tables | Pierre-Marie Pédrot |
| 2019-06-24 | [proof] Remove last case of optional `?poly` arguments. | Emilio Jesus Gallego Arias |
| 2019-06-24 | Use named records instead of tuples where `polymorphic` used to be. | Gaëtan Gilbert |
| 2019-06-24 | [proof] Move initial_euctx to proof_global | Emilio Jesus Gallego Arias |
| 2019-06-24 | [proof] API Documentation fixes. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [api] [proof] Move `discharge` type to vernac_ast where it is used. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [api] Remove `polymorphic` type alias, use labels instead. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [api] Move `locality` from `library` to `vernac`. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] [proof] Split proof kinds into per-layer components. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [proof] More uniformity in proof start labels. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [proof] Remove duplicated universe polymorphic from decl_kinds | Emilio Jesus Gallego Arias |
| 2019-06-24 | [proof] Remove redundant universe declaration information. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] Untabify. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] Turn Lemmas.info into a proper type with constructor. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [fixpoint] Remove code duplication in (co) fixpoint declaration. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] Reify proof information for recursive theorems. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] Reify info for implicits, univ_decls, prepare for rec_thms. | Emilio Jesus Gallego Arias |
| 2019-06-24 | Remove the export_seff flag from Declare API. | Pierre-Marie Pédrot |
| 2019-06-24 | Duplicate the type of constant entries in Proof_global. | Pierre-Marie Pédrot |
| 2019-06-20 | Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati... | Pierre-Marie Pédrot |
| 2019-06-19 | [Fail] Tweaks to implementation. | Emilio Jesus Gallego Arias |
| 2019-06-19 | [Fail] Simplify `Fail` implementation. | Emilio Jesus Gallego Arias |
| 2019-06-18 | [errors] remove "is_handled" logic, turn unhandled into anomalies | Emilio Jesus Gallego Arias |
| 2019-06-17 | Merge PR #10362: Kernel-side delaying of polymorphic opaque constants | Gaëtan Gilbert |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2019-06-17 | Allow to delay polymorphic opaque constants. | Pierre-Marie Pédrot |
| 2019-06-17 | Merge PR #10226: Simplify implicit_quantifiers | Emilio Jesus Gallego Arias |
| 2019-06-17 | [equations] [proof] Remove reference to evar_map | Emilio Jesus Gallego Arias |
| 2019-06-17 | [equations] [proof] Remove duplicate shrink function. | Emilio Jesus Gallego Arias |
| 2019-06-17 | [proof] Add proof save path for equations. | Emilio Jesus Gallego Arias |
