aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-24Merge PR #10394: [ide] chop sentences taking into account QUOTATION tokenPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: ppedrot
2019-06-21Merge PR #10416: Elpi 1.4.0Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-21Merge PR #9665: [dune] Enable optimization options in the compilation of the VM.Théo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-06-21[ci] overlay for coq-elpiEnrico Tassi
2019-06-21[docker] [ci] Update Elpi to version 1.4.0Enrico Tassi
2019-06-21[dune] Enable optimization options in the compilation of the VM.Emilio Jesus Gallego Arias
So far we didn't setup optimization flags for the VM in the Dune build, but time has come to experiment with such flags, we try -O3. Enabling `-flto` in the final binary build would be great, however this seems to break windows.
2019-06-21Merge PR #10414: Add Conda badge to README.mdThéo Zimmermann
Reviewed-by: Zimmi48
2019-06-21Add Conda badge to README.mdSamuel Lelièvre
2019-06-20Add output-coqtop test directory that runs output tests with coqtopJim Fehrle
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and ↵Pierre-Marie Pédrot
obligation ones. Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-06-20Fix coqdoc title: should be on a single line.Théo Zimmermann
Otherwise coqdoc doesn't understand it is still the title.
2019-06-19[Fail] Tweaks to implementation.Emilio Jesus Gallego Arias
We handle state restoration outside the main fail logic, as in the future it could be that vernac execution is fully functional so we could get rid of the second part.
2019-06-19[Fail] Simplify `Fail` implementation.Emilio Jesus Gallego Arias
We can now implement `Fail` in a direct style.
2019-06-19Merge PR #10380: [errors] remove "is_handled" logic, turn unhandled into ↵Gaëtan Gilbert
anomalies Reviewed-by: SkySkimmer Reviewed-by: gares
2019-06-19[test] unit tests for ide/coq_lex.mlEnrico Tassi
2019-06-19Removed backtracking and default variants of various functions and added ↵Michael Soegtrop
option combinators
2019-06-19[test-suite] support for unit-tests/ide/ tests linking coq.ideEnrico Tassi
2019-06-19[META] fix dependencies of coq.ideEnrico Tassi
2019-06-19[ide] chop sentences taking into account QUOTATION tokenEnrico Tassi
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations ↵Théo Zimmermann
in favor of "simple_intropattern" Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-18Merge PR #10398: Revert "Fix bug #5710"Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-06-18Removed "b" from function names in Bool.vMichael Soegtrop
Changed year in headers
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
We place the check for unhandled exceptions in the `is_anomaly` function, and consider all the exceptions non-handled by the printers always anomalies. This reworks the solution implemented in ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular `allow_uncaught` cannot be used anymore, all exceptions must install a printer. In order to pass the test-suite CI we also had to register some printers, that were not registered for no reason, forcing clients to call a post-processing step on errors.
2019-06-18Revert "Fix bug #5710"Vincent Laporte
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
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-17[ci] Overlays for #9645Emilio Jesus Gallego Arias
2019-06-17[proof] Respond to a comment by Pierre-MarieEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-15 07:18:21 +0000