aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-23test-suite: add approve-coqdoc to update all coqdoc output files at once.Hugo Herbelin
2021-04-19Merge PR #14068: [build] Remove leftovers of code signing / OSX IDE ↵coqbot-app[bot]
infrastructure Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-04-19Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be ↵Pierre-Marie Pédrot
set/unset as a modifier Reviewed-by: ppedrot
2021-04-19[build] Remove leftovers of codesigning / OSX IDe infrastructure.Emilio Jesus Gallego Arias
This is not used anymore, and after #14122 the makefile parts for the dmg generation are not used anymore. Closes #7476 .
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in ↵coqbot-app[bot]
Sphinx output Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-04-18Coqide: on MacOS X, allow the command key to be set/unset as a modifier.Hugo Herbelin
This is done by: - allowing the <Meta> gtk modifier (gtk internal name for Command) to be used as a modifier by default on MacOS X - printing it <cmd> in the preference window when on MacOS X
2021-04-18Merge PR #14122: Remove macOS dmg build.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-18Merge PR #14115: Change `Coqlib.lib_ref` to fail with `NameNotRegistered` ↵coqbot-app[bot]
instead of `UserError` Reviewed-by: ejgallego Ack-by: herbelin
2021-04-18Merge PR #14127: Pin docutils to 0.16.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-18Merge PR #14112: Cleanup useless environment manipulation in Class declarationcoqbot-app[bot]
Reviewed-by: ejgallego
2021-04-17Improve conversion chapter.Jim Fehrle
2021-04-17Disambiguate move tactics.Jim Fehrle
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Pin docutils to 0.16.Théo Zimmermann
Docutils 0.17 creates problem with our Sphinx rtd theme.
2021-04-17Remove superfluous sort.Jim Fehrle
Removing it makes no difference to the order of glossary entries, which is determined by the "for ... sorted" statement above.
2021-04-16[zify] bugfixFrederic Besson
- to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-16Remove macOS dmg build.Théo Zimmermann
Now that the platform takes care of it.
2021-04-16Catch UserError in Hipattern.match_with_equation in case name is not yet ↵Lasse Blaauwbroek
registered
2021-04-15Merge PR #14111: [ci] update elpi to 1.13.1coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: SkySkimmer
2021-04-14Update dev/ci/user-overlays/14111-gares-update-elpi.shEnrico Tassi
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2021-04-14Merge PR #14050: Remove remote counter systemcoqbot-app[bot]
Reviewed-by: gares Ack-by: ppedrot Ack-by: ejgallego
2021-04-14overlay fileEnrico Tassi
2021-04-14Merge PR #14045: Zify: more aggressive application of saturation rulesVincent Laporte
Reviewed-by: vbgl
2021-04-14Cleanup useless environment manipulation in Class declarationGaëtan Gilbert
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-14[ci] update elpi to 1.13.1Enrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:17:12 +0000