aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on ↵coqbot-app[bot]
red/orange background) Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-08Merge PR #14065: Documenting some parts of gramlib/grammar.mlcoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2021-04-08Merge PR #14095: Fix a GTK warning in CoqIDE introduced by #14063.coqbot-app[bot]
Reviewed-by: herbelin
2021-04-08Merge PR #14093: Register Ltac2 grammar entry as "ltac2" for the Print ↵coqbot-app[bot]
Grammar vernacular Reviewed-by: JasonGross
2021-04-08Gramlib: documentation of the recovery mechanism.Hugo Herbelin
2021-04-08Gramlib: some comments about how new rules are inserted.Hugo Herbelin
2021-04-08Gramlib: some comments about the main start/continue parsing loop.Hugo Herbelin
2021-04-08Merge PR #14080: CI-paramcoq: Re-enable nativecoqbot-app[bot]
Reviewed-by: ejgallego
2021-04-08Fix a GTK warning in CoqIDE introduced by #14063.Pierre-Marie Pédrot
The Variant entry was appearing twice, leading to a duplicate warning.
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
Fixes #14092: Print Grammar ltac2 should exist.
2021-04-08Merge PR #14027: Print type of offending expression in Ltac2 not-unit warning.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-08Merge PR #14062: Fixes #11690: wrongly toggled coqide printing matching flagPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-07Merge PR #14032: CI: don't output-synccoqbot-app[bot]
Reviewed-by: ejgallego
2021-04-07Merge PR #14078: Remove unused UnivProblem.Set.subst_univsPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-07Merge PR #14085: Dune: fix coqbyte shim after byterun->coqrun renamingcoqbot-app[bot]
Reviewed-by: ejgallego
2021-04-07Dune: fix coqbyte shim after byterun->coqrun renamingGaëtan Gilbert
2021-04-07Merge PR #14056: Miscellaneous mini-"typos" fixescoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: silene
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
Reviewed-by: olaure01 Ack-by: jfehrle
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-06Add a relative link to coq-core.Théo Zimmermann
2021-04-06Typo in ChoiceFacts.Hugo Herbelin
2021-04-06Missing dot in an error message.Hugo Herbelin
2021-04-06One catch-all's missing a noncritical; another is now useless (see 7efaf86).Hugo Herbelin
2021-04-06Standardizing spacing for {| ... |} in two files.Hugo Herbelin
2021-04-06Typo in a micromega comment.Hugo Herbelin
2021-04-06Uniformizing the "already exists" messagesHugo Herbelin
2021-04-06Make description of Pp.pr_enum more precise + spacing in pp.ml.Hugo Herbelin
2021-04-06CI-paramcoq: Re-enable nativeGaëtan Gilbert
It's an issue in paramcoq's test suite, which doesn't respect COQEXTRAFLAGS and so will be handled upstream (https://github.com/coq-community/paramcoq/pull/66)
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
From an OCaml library point of view.
2021-04-06Remove unused UnivProblem.Set.subst_univsGaëtan Gilbert
2021-04-06Merge PR #14042: Fix a bug in UnivProblemPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2021-04-06Merge PR #14063: Coqide: fixes #10720, highlight Variant keywordPierre-Marie Pédrot
2021-04-06Merge PR #14069: [coqpp] Add -helpPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-05Merge PR #13624: Fixing #13581: missing support for let-ins in arity of ↵coqbot-app[bot]
inductive types for extraction Reviewed-by: pi8027
2021-04-04More extraction tests for inductive types with let-ins.Hugo Herbelin
2021-04-04[coqpp] Add -helpEmilio Jesus Gallego Arias
Closes #9932
2021-04-04Adding change log for #13624.Hugo Herbelin
2021-04-04Fixing #13581: missing support for let-ins in arity of inductive types.Hugo Herbelin
At first view, the fix takes care about when to use the number of assumptions and when to also include local definitions, but I don't know all the details of the implementation to be absolutely sure.
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02Fixes #10720: highlighting Variant in CoqIDE.Hugo Herbelin
2021-04-02Fixes #11690: wrongly toggled coqide printing matching flag; moving raw->nested.Hugo Herbelin
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
add polynomial specifications of to_nat add changelog and doc entries
2021-04-01Merge PR #14053: [build] [ocamldebug] Update for byterun -> coqrun renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01[build] [ocamldebug] Update for byterun -> coqrun renamingEmilio Jesus Gallego Arias
Addendum to #14039 .
2021-04-01Merge PR #14039: [dune] Rename byterun to coqruncoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01Merge PR #14030: [doc] [dune] Some tweaks from #13617coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01[doc] [dune] Some tweaks from #13617Emilio Jesus Gallego Arias
Tweaks to docs that are independent / unrelated to that PR.
2021-04-01Merge PR #14047: [ci] Disable native compilation for paramcoqcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:21:06 +0000