aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: jashug
2019-05-13Merge PR #10079: [refman] Move Ltac examples to Ltac chapter.Vincent Laporte
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-05-12Merge PR #10083: Avoid trivial (u=u) constraints in AcyclicGraph.constraints_forEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-11Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS ↵Pierre-Marie Pédrot
+ adding a go-to-end binding + improving documentation Reviewed-by: gares Ack-by: herbelin Reviewed-by: ppedrot
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
Reviewed-by: herbelin
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10Merge PR #10058: Remove various circumvolutions from reduction behaviorsEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: maximedenes
2019-05-10Merge PR #10080: Define minimum Sphinx version in conf.py.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: vbgl
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl
2019-05-10Merge PR #10065: CI: run coqchk without -silentEmilio Jesus Gallego Arias
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-10Remove various circumvolutions from reduction behaviorsMaxime Dénès
Incidentally, this fixes #10056
2019-05-10CI: run coqchk without -silentGaëtan Gilbert
Since it's in its own job it won't pollute the log, and that way if some issue happens it will be easier to tell what's going on. I split the find and coqchk commands again as it's a bit confusing to parenthesize the pipe and `|| touch` otherwise.
2019-05-10Merge PR #10120: Clean-up: remove dead appveyor.sh file.Emilio Jesus Gallego Arias
2019-05-10Better title for the first example of the Ltac examples section.Théo Zimmermann
2019-05-09Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repoMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-05-09Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlabMichael Soegtrop
2019-05-09Improve the first two Ltac examples.Théo Zimmermann
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-09Rewording, language improvements.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
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-08[refman] Move all the Ltac examples to the Ltac chapter.Théo Zimmermann
The Detailed examples of tactics chapter can be removed when the remaining examples are moved closer to the definitions of the corresponding tactics. This commit also moves back the footnotes from the Tactics chapter at the end of the chapter, and removes an old footnote that doesn't matter anymore.
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-07Remove overlays for CompCert and VSTVincent Laporte
2019-05-07[nix-ci] Add coquelicot, improve flocqVincent Laporte
2019-05-07Add overlays for CompCert, VST, and coquelicotVincent Laporte
2019-05-07[Test-suite] Add output case for issue #9370Vincent Laporte
2019-05-07Improve field_simplify on fractions with constant denominatorthery
Before this patch, `x` was "simplified" to `x / 1`.
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ↵Clément Pit-Claudel
database. Reviewed-by: cpitclaudel
2019-05-07Avoid trivial (u=u) constraints in AcyclicGraph.constraints_forGaëtan Gilbert
Not sure how often this happens in practice but it seems it could.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-19 00:46:11 +0000