| Age | Commit message (Expand) | Author |
|---|
| 2017-12-08 | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès |
| 2017-12-07 | Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding) | Maxime Dénès |
| 2017-12-05 | Replacing Hashtbl.add by Hashtbl.replace in micromega cache building. | Hugo Herbelin |
| 2017-12-05 | Merge PR #890: Global universe declarations | Maxime Dénès |
| 2017-12-05 | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | Maxime Dénès |
| 2017-12-05 | Merge PR #6210: More complete not-fully-applied error messages, #6145 | Maxime Dénès |
| 2017-12-01 | Proper nametab handling of global universe names | Matthieu Sozeau |
| 2017-11-29 | Remove "obsolete_locality" and fix STM vernac classification. | Maxime Dénès |
| 2017-11-28 | more complete not-fully-applied error messages, #6145 | Paul Steckler |
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès |
| 2017-11-28 | Merge PR #6248: [api] Remove aliases of `Evar.t` | Maxime Dénès |
| 2017-11-27 | allow :: and , as infix ops | Paul Steckler |
| 2017-11-26 | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias |
| 2017-11-24 | Use Evarutil.has_undefined_evars for tactic has_evar. | Gaëtan Gilbert |
| 2017-11-24 | Use Entries.constant_universes_entry more. | Gaëtan Gilbert |
| 2017-11-24 | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert |
| 2017-11-24 | Stop exposing UState.universe_context and its Evd wrapper. | Gaëtan Gilbert |
| 2017-11-24 | Separate checking univ_decls and obtaining universe binder names. | Gaëtan Gilbert |
| 2017-11-24 | Extending further PR#6047 (system to register printers for Ltac values). | Hugo Herbelin |
| 2017-11-24 | Printing again "intros **" as "intros" by default. | Hugo Herbelin |
| 2017-11-24 | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | Maxime Dénès |
| 2017-11-24 | Merge PR #486: Make some functions on terms more robust w.r.t new term constr... | Maxime Dénès |
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès |
| 2017-11-24 | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | Maxime Dénès |
| 2017-11-23 | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès |
| 2017-11-23 | Merge PR #6186: [api] Miscellaneous consolidation. | Maxime Dénès |
| 2017-11-23 | Recognizing Z in romega up to conversion. | Hugo Herbelin |
| 2017-11-23 | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin |
| 2017-11-23 | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin |
| 2017-11-23 | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès |
| 2017-11-22 | [plugin] Remove LocalityFixme über hack. | Emilio Jesus Gallego Arias |
| 2017-11-22 | allow whitespace around infix op | Paul Steckler |
| 2017-11-22 | use OCaml criteria for infix ops, #6212 | Paul Steckler |
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias |
| 2017-11-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias |
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias |
| 2017-11-21 | Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API. | Maxime Dénès |
| 2017-11-21 | Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses | Maxime Dénès |
| 2017-11-20 | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin |
| 2017-11-20 | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state. | Maxime Dénès |
| 2017-11-20 | Merge PR #6161: Fix micromega.ml to match generated file and enforce match in... | Maxime Dénès |
| 2017-11-19 | Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Gaëtan Gilbert |
| 2017-11-19 | [plugins] Prepare plugin API for functional handling of state. | Emilio Jesus Gallego Arias |
| 2017-11-19 | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias |
| 2017-11-16 | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends. | Maxime Dénès |
| 2017-11-16 | Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2 | Maxime Dénès |
| 2017-11-16 | Fix micromega.ml to match generated file and enforce match in make. | Gaëtan Gilbert |
| 2017-11-15 | Fixing printing of tactics encapsulated as tacarg with Tacexp. | Hugo Herbelin |
| 2017-11-15 | Using "l" printer for glob_constr, like for constr. | Hugo Herbelin |
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias |
