aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-18Merge PR #10398: Revert "Fix bug #5710"Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-06-18Revert "Fix bug #5710"Vincent Laporte
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
2019-06-18Merge PR #9977: [dune] Support for coqide as an ocamldebug target.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ↵Maxime Dénès
local fix/cofix (#10197) Reviewed-by: maximedenes
2019-06-17Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of ↵Clément Pit-Claudel
#10205. Reviewed-by: cpitclaudel
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-06-17Merge PR #10320: Update headers to the new year.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-17Update copyright years outside of headers.Théo Zimmermann
These were found with the following command: $ git grep "1999-" | grep -v "2019"
2019-06-17Clean-up CREDITS file.Théo Zimmermann
Remove mentions of removed plugins. Remove copyright years to avoid them going out of sync. Fix explanation of the license of the documentation.
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
Remove other types of lines before copyright headers.
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
Most of these files were introduced after #6543 but used older headers copied from somewhere else.
2019-06-17Update py-style headers to new year.Théo Zimmermann
2019-06-17Update c-style headers to new year.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Update change-header script to support updating more than just files with ↵Théo Zimmermann
ml-style headers.
2019-06-17Adding overlays.Pierre-Marie Pédrot
2019-06-17Clean up the code adding monomorphic global constraints in Safe_typing.Pierre-Marie Pédrot
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
This enforces more invariants statically.
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
We had to move the private opaque constraints out of the constant declaration into the opaque table. The API is not very pretty yet due to a pervasive confusion between monomorphic global constraints and polymorphic local ones, but once we get rid of futures in the kernel this should be magically solved.
2019-06-17Merge PR #10226: Simplify implicit_quantifiersEmilio Jesus Gallego Arias
Reviewed-by: herbelin
2019-06-17Merge PR #10382: Ensuring that regular expression filtering in CI (iris) ↵Gaëtan Gilbert
works on MacOS X Reviewed-by: SkySkimmer
2019-06-17[dune] Support for coqide as an ocamldebug target.Emilio Jesus Gallego Arias
Works fine here, cc: #9975
2019-06-17Merge PR #10332: test suite: don't try to coqchk failed testsEnrico Tassi
Reviewed-by: maximedenes
2019-06-17Merge PR #10368: Update, expand, and document plugin tutorial 2Enrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: tlringer
2019-06-17Merge PR #10231: Adding location in warning telling implicit arguments ↵Emilio Jesus Gallego Arias
differ in term and type Reviewed-by: ejgallego Ack-by: jashug
2019-06-16Merge PR #10385: Changelog for 8.10+beta2.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-16Merge PR #10381: Fix #10090: Ltac1 destruct and Ltac2 destruct should do the ↵Emilio Jesus Gallego Arias
same thing. Reviewed-by: ejgallego
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-16Ensuring regexp filtering in ci works on MacOS X.Hugo Herbelin
Unfortunately, "+" regular expressions are not supported by default with MacOS X's sed. It is told that it would work with option -E though, but the syntax seems then different.
2019-06-16Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.Pierre-Marie Pédrot
The ML wrapper was wrongly calling induction instead of destruct.
2019-06-16Merge PR #10345: Fix #10339: Anomaly in Ltac2.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-16Overlays for Mtac2 and Equations.Hugo Herbelin
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-16Merge PR #10327: Fix bug #5710Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-06-16Merge PR #10355: [funind] Untabify; necessary to ease the review of ↵Pierre-Marie Pédrot
subsequent work. Reviewed-by: maximedenes
2019-06-15Merge PR #10040: Install byte version of coqidetop.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-15[dune] Install .byte version of coqidetop like for coqtop.Théo Zimmermann
2019-06-15Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
This allows to refer to them from other part of the manual without any ambiguity.
2019-06-14Merge PR #10376: Add a comment documenting what fontsupport.py is.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-14Add a comment documenting what fontsupport.py is.Théo Zimmermann
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
Reviewed-by: Zimmi48
2019-06-13Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-13Merge PR #10373: Add missing changelog entry for #10360.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
From the CHANGES file in branch v8.9.
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-13Update, expand, and document plugin tutorial 2Talia Ringer
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
Ack-by: ejgallego Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:28:30 +0000