| Age | Commit message (Expand) | Author |
|---|
| 2018-09-10 | Merge PR #8230: fix formulation of the Euclid Theorem in comment | Hugo Herbelin |
| 2018-09-10 | Declaring Scope prior to loading primitive printers. | Hugo Herbelin |
| 2018-09-10 | Adapting standard library to the introduction of "Declare Scope". | Hugo Herbelin |
| 2018-09-10 | Deprecate romega in favor of lia. | Vincent Laporte |
| 2018-09-07 | Bvector: add BVeq and some notations | Yishuai Li |
| 2018-09-07 | NArith: deprecate N2Bv_gen | Yishuai Li |
| 2018-09-06 | Bound proof-search in default program obligation tactic. | Matthieu Sozeau |
| 2018-08-31 | Make Numeral Notation follow Import, not Require | Jason Gross |
| 2018-08-31 | Fix numeral notation for a rebase on top of master | Jason Gross |
| 2018-08-31 | Decimal: scope name changed dec_(u)int_scope | Pierre Letouzey |
| 2018-08-31 | Numeral Notation for nat | Pierre Letouzey |
| 2018-08-31 | Numeral Notation: allow parsing from/to Decimal.int or Decimal.uint | Pierre Letouzey |
| 2018-08-31 | Prelude : update the comment about ML plugins loaded by Init | Pierre Letouzey |
| 2018-08-22 | Fix typo of caracterisation -> c*h*aracterisation | Siddharth Bhat |
| 2018-08-18 | Merge PR #8272: Fix typo in documentation, heigth --> height. | Théo Zimmermann |
| 2018-08-17 | Fix typo in documentation, heigth --> height. | Nick Lewycky |
| 2018-08-10 | one more fix to formulation of the Euclid Theorem in comment | Samuel Gruetter |
| 2018-08-09 | fix formulation of the Euclid Theorem in comment | Samuel Gruetter |
| 2018-08-01 | Merge PR #8169: NArith: add sized N2Bv | Hugo Herbelin |
| 2018-07-30 | Vector: expose ++ to user | Yishuai Li |
| 2018-07-26 | NArith: add sized N2Bv | Yishuai Li |
| 2018-07-25 | Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2) | Hugo Herbelin |
| 2018-07-24 | Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], [... | Hugo Herbelin |
| 2018-07-17 | Remove fourier plugin | Maxime Dénès |
| 2018-07-16 | Add additional lemmas about {String,Ascii}.eqb | Jason Gross |
| 2018-07-16 | Ascii.eqb and String.eqb | Pierre Letouzey |
| 2018-07-16 | bin,oct,hex conversions positive,Z,N,nat<->string | Jason Gross |
| 2018-07-10 | Fix typo in Init.Logic. | whitequark |
| 2018-07-02 | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau |
| 2018-06-29 | Splitting primitive numeral parser/printer for positive, N, Z into three files. | Hugo Herbelin |
| 2018-06-10 | Tweak printing boxes for unicode binders | Ralf Jung |
| 2018-06-05 | Merge PR #7690: Fixing typos in file Berardi.v | Pierre-Marie Pédrot |
| 2018-06-04 | Deprecate implicit tactic solving. | Pierre-Marie Pédrot |
| 2018-06-03 | Fixing typos in file Berardi.v | Hugo Herbelin |
| 2018-04-16 | Protecting against a "deprecated cofix" warning. | Hugo Herbelin |
| 2018-04-13 | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias |
| 2018-04-02 | Make OrderedTypeFullFacts a module functor | Simon Gregersen |
| 2018-03-09 | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès |
| 2018-03-09 | Merge PR #6155: Get rid of ' notation for Zpos in QArith | Maxime Dénès |
| 2018-03-09 | Merge PR #6937: Add empty compat file for Coq 8.8 | Maxime Dénès |
| 2018-03-08 | Merge PR #6522: Fix core hint database issue #6521 | Maxime Dénès |
| 2018-03-08 | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès |
| 2018-03-08 | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès |
| 2018-03-07 | [stdlib] Do not use “Require” inside sections | Vincent Laporte |
| 2018-03-07 | Add empty compat file for Coq 8.8 | Jason Gross |
| 2018-03-07 | Merge PR #6744: Add String.concat | Maxime Dénès |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès |
| 2018-03-04 | Remove all uses of Focus in standard library. | Théo Zimmermann |
| 2018-03-02 | Remove 8.5 compatibility support. | Théo Zimmermann |
| 2018-03-02 | Remove VOld compatibility flag. | Théo Zimmermann |
