| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2019-06-17 | [lemmas] Refactoring in saving goal. | Emilio Jesus Gallego Arias |
| 2019-06-17 | [proof] Remove terminator type, unifying regular and obligation ones. | Emilio Jesus Gallego Arias |
| 2019-06-17 | [proof] Move declaration hooks to DeclareDef. | Emilio Jesus Gallego Arias |
| 2019-06-17 | [proof] drop parameter from terminator type | Emilio Jesus Gallego Arias |
| 2019-06-17 | [proof] Unify obligation proof save path: Part I, declareObl | Emilio Jesus Gallego Arias |
| 2019-06-17 | [proofs] Store hooks in the proof object. | Emilio Jesus Gallego Arias |
| 2019-06-16 | Turning "manual_implicits" into a list of position in impargs.ml. | Hugo Herbelin |
| 2019-06-16 | Adding location in warning telling implicit arguments differ in term and type. | Hugo Herbelin |
| 2019-06-13 | Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLater | Enrico Tassi |
| 2019-06-12 | Merge PR #10180: `deprecated` attribute support for notations and syntactic d... | Théo Zimmermann |
| 2019-06-12 | Fix #9455: avoid update_global_env when unchanged Global.universes() | Gaëtan Gilbert |
| 2019-06-11 | Remove the side-effect role from the kernel. | Pierre-Marie Pédrot |
| 2019-06-11 | STM: encode in static types that vernac_when is only used when VtSideff | Gaëtan Gilbert |
| 2019-06-11 | Fix #10225 (Instance := {} accepts duplicate fields) | Gaëtan Gilbert |
| 2019-06-09 | [proof] Uniformize Proof_global API | Emilio Jesus Gallego Arias |
| 2019-06-09 | [save_proof] Make terminator API internal. | Emilio Jesus Gallego Arias |
| 2019-06-09 | [proof] Move proofs that have an associated constant to `Lemmas` | Emilio Jesus Gallego Arias |
| 2019-06-08 | Cleaning the status of Local Definition and similar. | Hugo Herbelin |
| 2019-06-08 | Adding a new kind of assumption to track assumption coming from "Context". | Hugo Herbelin |
| 2019-06-06 | Merge PR #10278: vernac_load doesn't get a ?proof argument | Emilio Jesus Gallego Arias |
| 2019-06-06 | Merge PR #8988: Towards unifying parsing/printing for universe instances and ... | Gaëtan Gilbert |
| 2019-06-06 | `deprecated` attribute support for notations and syntactic definitions | Maxime Dénès |
| 2019-06-05 | vernac_load doesn't get a ?proof argument | Gaëtan Gilbert |
| 2019-06-05 | Merge PR #10215: Refine typing of vernacular commands | Maxime Dénès |
| 2019-06-04 | [vernac] Interpret regular vernacs symbolically | Emilio Jesus Gallego Arias |
| 2019-06-04 | Merge PR #10265: Fix #10264: Singleton class field data is erroneous. | Matthieu Sozeau |
| 2019-06-04 | Simplify vernacentries calls to classes, remove unused args, reject deprecate... | Gaëtan Gilbert |
| 2019-06-04 | remove leftover comments | Enrico Tassi |
| 2019-06-04 | [classes] remove program mode from the new_instance_* APIs | Enrico Tassi |
| 2019-06-04 | [vernac] more precise types for Add Morph, Instance, and Function | Enrico Tassi |
| 2019-06-04 | [vernac] remove VtMaybeOpenProof | Enrico Tassi |
| 2019-06-04 | VernacExtend produces vernac_interp_phase ADT (old name functional_vernac) | Gaëtan Gilbert |
