aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-30[vm] x86_64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376 from OCaml VM
2019-04-29Merge PR #9983: Hypothesis conversion allocates a single evarHugo Herbelin
Reviewed-by: gares Ack-by: herbelin
2019-04-29Merge PR #9946: Add some entries to .mailmapEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-04-29Add some entries to .mailmapJason Gross
I ran `git shortlog -nse | sed s'/^[ 0-9\t]*//g' | sort | less` and manually inspected the result for duplicates. Then I used ```bash git shortlog -nse | sed s'/^[ 0-9\t]*//g' | sort | sed s'/<.*>//g' | uniq -c | grep -v '^ *1 ' ``` to check that there were no remaining duplicates.
2019-04-29Merge PR #9987: Fix #9180 by reverting #9249 and #8187Emilio Jesus Gallego Arias
Reviewed-by: maximedenes
2019-04-29Merge PR #9646: [proof] Fix proof bullet error helper which was implemented ↵Maxime Dénès
as a hook Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: erikmd Ack-by: gares Ack-by: jfehrle
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ↵Maxime Dénès
not to be used. Ack-by: ejgallego Ack-by: gares Reviewed-by: maximedenes
2019-04-29Merge PR #9775: inferCumulativity: shortcut for all-Invariant inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-29Merge PR #10014: CoqIDE: load coqiderc after coqide.keysPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-29Merge PR #10007: Amending sphinx-on-windows fix in #9819 so that it does not ↵Vincent Laporte
trigger a warning on MacOS X (and other BSD systems). Ack-by: SkySkimmer Ack-by: herbelin Reviewed-by: vbgl
2019-04-29Merge PR #10011: [refman] Fix typo.Vincent Laporte
Reviewed-by: vbgl
2019-04-29Merge PR #10018: Document unshelve (#3225)Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-29Merge PR #10021: More robust timing test.Enrico Tassi
Reviewed-by: gares
2019-04-29Test-suite: add a case for issue #9180Vincent Laporte
2019-04-29Revert #8187Vincent Laporte
2019-04-29Revert #9249Vincent Laporte
2019-04-29More robust timing test.Jason Gross
2019-04-29Merge PR #9997: CoqIDE: fix open-file dialog and icons on macOSEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2019-04-29[meta] [dune] Fix discrepancies in plugin namesEmilio Jesus Gallego Arias
We have some discrepancy with the package names for plugins in the META / Dune case. This PR fixes it. At some point there was a need for plugin package names having to be named as their directories. I think this is not true anymore, but taking the "dir_name == package_name" convention just in case.
2019-04-29Document unshelve (#3225)Paolo G. Giarrusso
I believe this is the appropriate place for users to read about this, even tho `unshelve` is technically a tactical. This example was explicitly requested in #3225 and is commonly used in both Iris (and was documented in the changelog at the time).
2019-04-28Merge PR #10010: [ci/gitlab] Remove after_switch message (not useful anymore).Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-28Merge PR #9605: [coq_makefile] Enforce warn_error for plugins.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares
2019-04-27Updating CHANGES.Hugo Herbelin
2019-04-27CoqIDE, cosmetic: removing obsolete comments.Hugo Herbelin
There is no more uses of "old style preferences" but the comment was still there.
2019-04-27CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899).Hugo Herbelin
This avoids the modifiers keys to overwrite changes made in coqide.keys.
2019-04-27Minor doc improvement.Théo Zimmermann
2019-04-27[refman] Fix typo.Théo Zimmermann
Noticed by Maxime Dénès.
2019-04-27[ci/gitlab] Remove after_switch message (not useful anymore).Théo Zimmermann
This was put in place for @coqbot to detect runner failures, but now the strategy is different.
2019-04-27Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.Hugo Herbelin
Indeed, MacOS has a BSD uname and BSD uname does not support the -o option. Based on the following resources about uname compatility: https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux https://en.wikipedia.org/wiki/Uname
2019-04-26Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-26Merge PR #9981: [dune] Build coqc.byte executable.Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-04-26Merge PR #9990: [opam] Use version to provide better package bounds.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-26Merge PR #10001: Add a typing colon in the output of the Search ssreflect ↵Enrico Tassi
vernacular Reviewed-by: gares
2019-04-26[opam] Use version to provide better package bounds.Emilio Jesus Gallego Arias
I copied this from Ralf Jung's submission to the Coq Package index, let's see if it works.
2019-04-25Merge PR #9999: Fix PKG in ide/.merlin.in for gtk3Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-25CoqIDE: install icons on macOSVincent Laporte
2019-04-25inferCumulativity: shortcut for all-Invariant inductivesGaëtan Gilbert
2019-04-25Add a typing colon in the output of the Search ssreflect vernacularErik Martin-Dorel
See also PR math-comp/math-comp#73
2019-04-25Fix PKG in ide/.merlin.in for gtk3Gaëtan Gilbert
2019-04-25CoqIDE: fix open-file dialog on macOSVincent Laporte
2019-04-25coq_makefile: do not pass -opt/-byte to coqc (fix #9974)Enrico Tassi
2019-04-24Merge PR #9988: [refman] Properly define token regexp.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24Merge PR #9989: [refman] Fix a quoting problem.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24[refman] Fix a quoting problem.Théo Zimmermann
2019-04-24[refman] Properly define token regexp.Théo Zimmermann
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974
2019-04-24Fix proof bullet error helper (nosuchgoal)Gaëtan Gilbert
The [int] is incorrect for list focusing, we could work a bit harder to fix that. It's only used for pluralisation in the error message "no such goal(s)" so we could also ignore the issue.
2019-04-24[proof] Fix proof bullet error helper which was implemented as a hookEmilio Jesus Gallego Arias
We add the information on the proper layer by catching the low-level exception.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-06 03:29:21 +0000