aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-10Remove ref from some implicit_discharge_requestJasper Hugunin
2019-05-10Simplify dispose_implicitsJasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 18:51:04 +0000