| Age | Commit message (Expand) | Author |
|---|
| 2018-09-11 | Merge PR #7135: Introducing an explicit `Declare Scope` command | Emilio Jesus Gallego Arias |
| 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-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 | Numeral Notation for nat | Pierre Letouzey |
| 2018-08-22 | Fix typo of caracterisation -> c*h*aracterisation | Siddharth Bhat |
| 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-07-16 | Ascii.eqb and String.eqb | Pierre Letouzey |
| 2018-06-29 | Splitting primitive numeral parser/printer for positive, N, Z into three files. | Hugo Herbelin |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès |
| 2018-03-02 | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2018-02-20 | Decimal goodies : conversion to/from Coq strings | Pierre Letouzey |
| 2018-02-20 | Decimal: proofs that conversions from/to nat,N,Z are bijections | Pierre Letouzey |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin |
| 2017-07-26 | Merge PR #845: Add Z.mod_div lemma to standard library. | Maxime Dénès |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-29 | Add Z.mod_div lemma to standard library. | Russell O'Connor |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ... | Matej Kosik |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond |
| 2016-09-28 | ZDivEucl: notations in different scope to avoid a warning | Pierre Letouzey |
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ... | Hugo Herbelin |
| 2016-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2016-06-16 | Remove unneded hints in NZGcd | Matthieu Sozeau |
| 2016-06-16 | Typeclasses: stdlib fixes for new search algorithm | Matthieu Sozeau |
| 2016-06-16 | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels. | Hugo Herbelin |
| 2016-05-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-04 | NPeano : improve compatibility for this deprecated file via compat notations | Pierre Letouzey |
| 2016-04-27 | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ... | Hugo Herbelin |
| 2016-04-27 | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels. | Hugo Herbelin |
| 2016-03-04 | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot |
| 2016-02-26 | Qcanon : implement some old suggestions by C. Auger | Pierre Letouzey |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-15 | Failing on unbound notation variable in notation level modifiers | Hugo Herbelin |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-10-10 | Give the same argument name for the record binder of type class | Matthieu Sozeau |
| 2014-10-10 | Fix segfault in native compiler on int31 division. | Maxime Dénès |
| 2014-10-01 | argument flip of Cyclic31.nshiftr and Cyclic31.nshiftl | Pierre Boutillier |
| 2014-10-01 | Simpl less (so that cbn will not simpl too much) | Pierre Boutillier |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
