aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-10Add overlays for coq/coq#10052.Pierre-Marie Pédrot
2019-05-10Fast-path for reordering of a single closed variable.Pierre-Marie Pédrot
Doesn't seem to matter in practice, but it doesn't hurt either.
2019-05-10Take advantage of the ordering / conversion check split.Pierre-Marie Pédrot
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one.
2019-05-10Logic.convert_hyp now takes an environment as an argument.Pierre-Marie Pédrot
This prevents having to call global functions, for no good reason. We also seize the opportunity to name the check argument.
2019-05-10Cleanup of Logic.convert_hyp.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:58:33 +0000