aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
2020-04-21Update common.edit_mlg and fullGrammar following #12038.Théo Zimmermann
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-21Merge PR #12060: CoqIDE: Disable client-side decoration on WindowsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-21Merge PR #12113: Contributing guide improvementsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-21Merge PR #12137: Fix VST after PrincetonUniversity/VST#402Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of ↵Pierre-Marie Pédrot
custom induction scheme Reviewed-by: ppedrot
2020-04-21Merge PR #12014: [stdlib] Add properties of operations on vectorsHugo Herbelin
Reviewed-by: herbelin
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
Reviewed-by: herbelin
2020-04-21Fix VST after PrincetonUniversity/VST#402Gaëtan Gilbert
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
2020-04-20Merge PR #12038: Improve undeclared goption key messages.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12026: Granting coqdoc wish #7093: definitions link to themselves ↵Lysxia
so as to give access to their url Reviewed-by: Lysxia
2020-04-20Adding change log for PR #12026 (definitions in coqdoc link to themselves).Hugo Herbelin
2020-04-20Granting coqdoc wish #7093 (definitions link to themselves).Hugo Herbelin
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-04-20TIMEFMT: Display the output file nameJason Gross
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
2020-04-20Merge PR #12091: Adding highlighting of the target of a internal link in ↵Lysxia
default coqdoc CSS Reviewed-by: Lysxia
2020-04-20Adding change log.Hugo Herbelin
2020-04-20Adding highlighting of the target of a internal link in coqdoc CSS.Hugo Herbelin
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-20Use polymorphic record for Vernacentries.iter_tableGaëtan Gilbert
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-20Merge PR #12123: Don't create index entries for the name "_"Théo Zimmermann
Reviewed-by: cpitclaudel
2020-04-20Merge PR #12125: Fix Makefile warning: undefined variable '*'Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Change log for PR #12045.Hugo Herbelin
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-20Merge PR #12106: Coqide: Apply style scheme and language settings to the ↵Pierre-Marie Pédrot
three sourceview buffers. Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-20Merge PR #12077: Update .mailmapThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-19Merge PR #12074: added changelog for PR 12044Jason Gross
Reviewed-by: JasonGross
2020-04-19added changelog for PR 12044ilya
Update doc/changelog/10-standard-library/12044-issue-12015.rst Co-Authored-By: Jason Gross <jasongross9@gmail.com> Apply suggestions from code review
2020-04-19Update .mailmapJason Gross
2020-04-19Fix Makefile warning: undefined variable '*'Jason Gross
We fix ``` Makefile.build:222: warning: undefined variable '*' ``` by not passing a time format including a Makefile variable when not inside a target (and whether or not the command succeeds should not depend on the particular format in any case, and all we are testing for is whether or not the command exists and supports `-f`).
2020-04-19Don't create index entries for the name "_"Jim Fehrle
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables ↵Lysxia
(incidentally fixes #7697) Reviewed-by: Lysxia
2020-04-19CoqIDE: Adding a short documentation on style/theme customization.Hugo Herbelin
2020-04-17Coqide: Apply style scheme and language to the three buffers.Hugo Herbelin
It was previously only applied to the script buffer.
2020-04-17Merge PR #12111: CI: Ignore spurious errors in validate jobsThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-17Merge PR #11976: Deprecate the omega tacticThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-17Merge PR #12112: Adapt linter documentation to the recent improvements of ↵Gaëtan Gilbert
the pre-commit hook. Reviewed-by: SkySkimmer
2020-04-17Adapt linter documentation to the recent improvements of the pre-commit hook.Théo Zimmermann
2020-04-17More documentation on draft PRs.Théo Zimmermann
2020-04-17Contributing guide: turn some sub-sections into sub-sub-sections.Théo Zimmermann
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-17CI: Ignore spurious errors in validate jobsGaëtan Gilbert
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11963: NativeCompute Timing: Use real, not user timePierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to ↵Pierre-Marie Pédrot
primitive projections Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
User time is unreliable for `native_compute`. Also output time spent in conversion to native code, just in case that is ever slow. Note that this also removes spurious newlines in the output. Fixes #11962
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:46:15 +0000