aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-04-16Remove macOS dmg build.Théo Zimmermann
2021-04-16Catch UserError in Hipattern.match_with_equation in case name is not yet regi...Lasse Blaauwbroek
2021-04-15Merge PR #14111: [ci] update elpi to 1.13.1coqbot-app[bot]
2021-04-14Update dev/ci/user-overlays/14111-gares-update-elpi.shEnrico Tassi
2021-04-14Merge PR #14050: Remove remote counter systemcoqbot-app[bot]
2021-04-14overlay fileEnrico Tassi
2021-04-14Merge PR #14045: Zify: more aggressive application of saturation rulesVincent Laporte
2021-04-14Cleanup useless environment manipulation in Class declarationGaëtan Gilbert
2021-04-14Add test for -schedule-vio-checkingGaëtan Gilbert
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
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]
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
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]
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]
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
2021-04-12Merge PR #14046: make critical sections safe in the presence of exceptionscoqbot-app[bot]
2021-04-12[zify] better error reportingBESSON Frederic
2021-04-10Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymorecoqbot-app[bot]
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/or...coqbot-app[bot]
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
2021-04-08remove `with hintdb` variant of Ltac2 `unify`, becauseSamuel Gruetter
2021-04-08Merge PR #14065: Documenting some parts of gramlib/grammar.mlcoqbot-app[bot]
2021-04-08Merge PR #14095: Fix a GTK warning in CoqIDE introduced by #14063.coqbot-app[bot]
2021-04-08Merge PR #14093: Register Ltac2 grammar entry as "ltac2" for the Print Gramma...coqbot-app[bot]
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]
2021-04-08Fix a GTK warning in CoqIDE introduced by #14063.Pierre-Marie Pédrot
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
2021-04-08Merge PR #14027: Print type of offending expression in Ltac2 not-unit warning.coqbot-app[bot]
2021-04-08Merge PR #14062: Fixes #11690: wrongly toggled coqide printing matching flagPierre-Marie Pédrot
2021-04-07unify for Ltac2Samuel Gruetter
2021-04-07overlayEnrico Tassi
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-07cleanup: remove confusing sharingEnrico Tassi
2021-04-07cleanup: less exceptions, removal of try_interp_name_aliasEnrico Tassi
2021-04-07Merge PR #14032: CI: don't output-synccoqbot-app[bot]
2021-04-07Merge PR #14078: Remove unused UnivProblem.Set.subst_univsPierre-Marie Pédrot
2021-04-07Merge PR #14085: Dune: fix coqbyte shim after byterun->coqrun renamingcoqbot-app[bot]
2021-04-07Dune: fix coqbyte shim after byterun->coqrun renamingGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:43:50 +0000