aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-10Merge PR #10120: Clean-up: remove dead appveyor.sh file.Emilio Jesus Gallego Arias
2019-05-09Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repoMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ↵Maxime Dénès
specification Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-05-09Merge PR #10126: Ignore generated dune file for Ltac2Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-09Ignore generated dune file for Ltac2Vincent Laporte
2019-05-09Merge PR #10082: Fix PLUGINSVO computation after ltac2 integrationMaxime Dénès
Reviewed-by: maximedenes
2019-05-09Merge PR #10069: Do not use the constant stack in ↵Hugo Herbelin
whd_betaiota_deltazeta_for_iota_state. Reviewed-by: herbelin
2019-05-08Remove ltac2 add-on from Windows installer now that it is in the main Coq ↵Théo Zimmermann
package.
2019-05-08Clean-up: remove dead appveyor.sh file.Théo Zimmermann
2019-05-08Merge PR #10087: Added description of QThéo Zimmermann
Reviewed-by: Zimmi48
2019-05-08Merge PR #10086: Fix gitignore for ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-08Merge PR #10119: Show diffs in error messages only if Diffs is enabledGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-07Show diffs in error messages only if Diffs is enabledJim Fehrle
2019-05-07Added "Recursively" for the R optionRobert Rand
2019-05-07Added description of QRobert Rand
Note that this description is identical to that of R. R should maybe start with the word "Recursively"?
2019-05-07Fix gitignore for ltac2Gaëtan Gilbert
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ↵Clément Pit-Claudel
database. Reviewed-by: cpitclaudel
2019-05-07Merge PR #10016: [test-suite] Remove a test with a Timeout that fails ↵Vincent Laporte
frequently on CI. Reviewed-by: vbgl
2019-05-07Fix PLUGINSVO computation after ltac2 integrationGaëtan Gilbert
Avoid looking at random installed packages in -local mode.
2019-05-07Remove ppedrot/ltac2 from CI after integration in main repoGaëtan Gilbert
2019-05-07Merge PR #10053: Document change_no_check variantsThéo Zimmermann
Ack-by: JasonGross Reviewed-by: Zimmi48
2019-05-07Merge PR #10075: [Record] Une a record to gather field declaration attributesEnrico Tassi
Reviewed-by: gares
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
Ack-by: JasonGross Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: jfehrle Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-05-07[refman] Add a note reminding about the typeclass_instances database.Théo Zimmermann
Closes #10072.
2019-05-07Merge PR #10063: CoqIDE: recognize qualified identifiers as words.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-07Add overlays.Pierre-Marie Pédrot
2019-05-07Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
There is no point, it is always called with refolding turned off.
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-05-07[Record] DeforestationVincent Laporte
2019-05-07[Canonical structures] DeforestationVincent Laporte
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.
2019-05-06Merge PR #10068: Coqchk: encapsulating an anomaly NotConvertible into a ↵Pierre-Marie Pédrot
proper user-level typing error Reviewed-by: ppedrot
2019-05-06Merge PR #9964: Unreleased changelog folderVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Reviewed-by: vbgl
2019-05-06Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.Hugo Herbelin
Detected incidentally in "validate" check for #8893.
2019-05-05Add changelog entry about moving changelog to refman.Théo Zimmermann
2019-05-05[make] build unreleased.rstEnrico Tassi
2019-05-05Create categories in changelog.Théo Zimmermann
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
Move existing entries.
2019-05-05Merge PR #10059: Fixing bugs introduced in change_no_checkPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear ↵Pierre-Marie Pédrot
as assumptions Ack-by: RalfJung Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot Ack-by: robbertkrebbers
2019-05-04Merge PR #10012: Document convert_concl_no_check (#3225)Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2019-05-04Merge PR #10057: Fix #10054: Numeral Notations without the ltac plugin.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-03CoqIDE: recognize qualified identifiers as words.Jasper Hugunin
Fixes coq/coq#10062. The implementation is rough, and does not deal with leading, trailing, or doubled periods, but the same can be said of the current handling of leading numbers or primes.
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
(Merge of the initial version with #9983 was broken)
2019-05-03Updating CHANGES.Hugo Herbelin
2019-05-03Merge PR #9984: Add PairUsualDecidableTypeFullThéo Zimmermann
Reviewed-by: herbelin
2019-05-03Remove now useless commented codePierre Roux
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
There are three implementations of this primitive: * one in OCaml on 63 bits integer in kernel/uint63_amd64.ml * one in OCaml on Int64 in kernel/uint63_x86.ml * one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h Its specification is the axiom `diveucl_21_spec` in theories/Numbers/Cyclic/Int63/Int63.v * comment the implementations with loop invariants to enable an easy pen&paper proof of correctness (note to reviewers: the one in uint63_amd64.ml might be the easiest to read) * make sure the three implementations are equivalent * fix the specification in Int63.v (only the lowest part of the result is actually returned) * make a little optimisation in div21 enabled by the proof of correctness (cmp is computed at the end of the first loop rather than at the beginning, potentially saving one loop iteration while remaining correct) * update the proofs in Int63.v and Cyclic63.v to take into account the new specifiation of div21 * add a test
2019-05-03Merge PR #10025: Fix #9994: `revert dependent` is extremely slow.Vincent Laporte
Ack-by: ppedrot Reviewed-by: vbgl
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 02:39:48 +0000