aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-20Remove mod_constraints field of module bodyGaëtan Gilbert
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-19A library on cyclic permutations: CPermutationOlivier Laurent
(following the pattern of Permutation.v)
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-19Use binary integers for Cauchy realsVincent Semeria
2020-04-19Fix a typoPierre Roux
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-19remove useless hypothesis in NoDup_Permutation_bisOlivier Laurent
(thanks to new NoDup_incl_NoDup)
2020-04-18Make multiplication of Cauchy reals transparent and accelerate itVincent Semeria
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-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-16Checker: factorize handling of typing flagsGaëtan Gilbert
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-04-16Merge PR #12069: [gitlab-ci] Only run Windows jobs when ONLY_WINDOWS ↵Gaëtan Gilbert
variable is true. Reviewed-by: gares
2020-04-16CoqIDE: Disable client-side decoration on WindowsAttila Gáspár
2020-04-16Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-16Merge PR #11999: [proof] Merge `Proof_global` into `Declare`Gaëtan Gilbert
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15Adding change log for PR #12033 (hyperlinks on binders for coqdoc).Hugo Herbelin
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
This provides linking, appropriate coloring and appropriate hovering in coqdoc documents. In particular, this fixes #7697.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 19:26:38 +0000