| Age | Commit message (Expand) | Author |
|---|
| 2020-12-03 | Ascii: add leb and ltb | Yishuai Li |
| 2020-11-09 | Merge PR #13173: Lint stdlib with -mangle-names #4 | coqbot-app[bot] |
| 2020-10-11 | Modify Strings/String.v to compile with -mangle-names | Jasper Hugunin |
| 2020-10-11 | Modify Strings/Ascii.v to compile with -mangle-names | Jasper Hugunin |
| 2020-10-05 | Adapting theories to unused pattern-matching variable warning. | Hugo Herbelin |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2020-01-08 | Avoid hardcoded paths in extraction | Maxime Dénès |
| 2019-06-17 | Update headers of files that were stuck on older headers. | Théo Zimmermann |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2019-05-25 | Modifying theories to preferably use the "[= ]" syntax, and, | Hugo Herbelin |
| 2018-12-12 | Merge PR #9087: Add CI job building stdlib with `async-proofs on` | Emilio Jesus Gallego Arias |
| 2018-12-12 | Avoid Fixpoint without struct nor body in stdlib | Maxime Dénès |
| 2018-11-28 | Byte.v: use right-associative tuples in bits | Jason Gross |
| 2018-11-28 | Proofs to ensure that conversions round-trip | Jason Gross |
| 2018-11-28 | Speed up Byte | Jason Gross |
| 2018-11-28 | Add `String Notation` vernacular like `Numeral Notation` | Jason Gross |
| 2018-11-11 | Merge PR #8795: Encapsulating declarations of primitive string syntax in a mo... | Jason Gross |
| 2018-10-29 | NArith: add lemmas about numbers and vectors | Yishuai Li |
| 2018-10-23 | Encapsulating declarations of primitive string syntax in a module. | Hugo Herbelin |
| 2018-10-17 | Strings: add ByteVector | Yishuai Li |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias |
| 2018-09-10 | Declaring Scope prior to loading primitive printers. | Hugo Herbelin |
| 2018-07-25 | Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2) | Hugo Herbelin |
| 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-03-07 | Merge PR #6744: Add String.concat | Maxime Dénès |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2018-02-24 | Add String.concat | Jason Gross |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 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-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-09-17 | Add some missing Proof statements. | Guillaume Melquiond |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2011-10-22 | Fixing Equality.injectable which did not detect an equality without | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-04 | Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-... | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-27 | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey |
