aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-19Check for existence before using `Global.lookup_constant` instead of ↵Lasse Blaauwbroek
catching `Not_found` `Global.lookup_constant` fails with an assertion instead of `Not_found`. Some code relied upon `Not_found`.
2021-04-14Merge PR #14050: Remove remote counter systemcoqbot-app[bot]
Reviewed-by: gares Ack-by: ppedrot Ack-by: ejgallego
2021-04-14Merge PR #14045: Zify: more aggressive application of saturation rulesVincent Laporte
Reviewed-by: vbgl
2021-04-14Add test for -schedule-vio-checkingGaëtan Gilbert
Close #14074
2021-04-14Overlay for no remote counterGaëtan Gilbert
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-14Put async worker id in universe namesGaëtan Gilbert
This removes the need for the remote counter.
2021-04-13Merge PR #14024: [coqdep] error on non-existent and unreadable filescoqbot-app[bot]
Reviewed-by: gares Ack-by: jfehrle Ack-by: ejgallego
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
The role of the `zify_saturate` tactic is to augment the goal with positivity constraints. The premisses were previously obtained from the context. If they are not present, we instantiate the saturation lemma anyway. Also, - Remove saturation rules for Z.mul, the reasoning is performed by lia/nia - Run zify_saturate after zify_to_euclidean_division_equations - Better lemma for Z.power - Ensure that lemma are generated once Co-authored-by: Andrej Dudenhefner <mrhaandi> Closes #12184, #11656
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
Print an error message and return non-zero status for non-existing or unreadable files. Unknown options produce a warning and are otherwise ignored. Fixes #14023
2021-04-12Fix unknown -vos option for coqdep_boot introduced in PR #11074Hendrik Tews
2021-04-12Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.coqbot-app[bot]
Reviewed-by: jfehrle
2021-04-12Remove omega from doc_grammar files.Théo Zimmermann
2021-04-12Gitignore update for doc_grammar.Théo Zimmermann
2021-04-12Merge PR #14038: [dune] [coqdoc] Install coqdoc.sty also in share/texmfcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
Reviewed-by: vbgl
2021-04-12Merge PR #14046: make critical sections safe in the presence of exceptionscoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: gares Ack-by: SkySkimmer Ack-by: gadmm
2021-04-12[zify] better error reportingBESSON Frederic
The vernacular command takes a reference instead of a constr. Moreover, the head symbol is checked i.e Add Zify InjTyp ref checks that the referenced term has type Intyp X1 ... Xn Closes #14054, #13242 Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
2021-04-10Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymorecoqbot-app[bot]
Reviewed-by: jfehrle
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-10Fix link in doc/cic.rst, there is no Credits chapter anymoreYannick Forster
2021-04-09Make critical sections safe in the presence of exceptionsLasse Blaauwbroek
We introduce the `with_lock` combinator that locks a mutex in an atomic fashion. This ensures that exceptions thrown by signals will not leave the system in a deadlocked state.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:16:07 +0000