aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-09-10Moving configuration of coqide.keys to the coqide executable.Hugo Herbelin
2019-09-10Using GTK+ PRIMARY to factorize CoqIDE keys between MacOS and others.Hugo Herbelin
This concerns zooming, undoing, displaying preferences.
2019-09-10Hack to have the "ready" status bar message not hiding flash notices.Hugo Herbelin
2019-09-10Being more informative on the steps of selection of the preference file.Hugo Herbelin
2019-09-10CoqIDE: Letting flash notices being treated sequentially.Hugo Herbelin
2019-09-10Making a bit clearer that CoqIDE modifier menu is for global modifier change.Hugo Herbelin
Indeed, one can change each item locally, but the preference menu is only for changing the modifiers of a whole menu at once.
2019-09-10Fixing #8269: adding callback on changed modifiers only after pref loading.Hugo Herbelin
Otherwise, probably for the reason suspected in [1], loading the preference file (coqiderc) is interpreted as a change of the modifiers, and this overrides what the more fine-grained preferences (coqide.keys) was telling. [1] https://github.com/coq/coq/issues/8269#issuecomment-415971367
2019-09-10Indentation in configure.ml.Hugo Herbelin
2019-09-10Merge PR #9406: [stdlib] Do not put INR_eq in the “real” hint databasePierre-Marie Pédrot
Reviewed-by: silene
2019-09-10Switch maintenance of `ring` to a teamMaxime Dénès
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2019-09-09Merge PR #10605: [toplevel] Make all argument lists to be in user-declared ↵Hugo Herbelin
order. Reviewed-by: herbelin
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-09-08more precise error messages for `Add Ring`Samuel Gruetter
2019-09-07overlay for elpiEnrico Tassi
2019-09-07update elpi to 1.7Enrico Tassi
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2019-09-05Merge PR #10730: Add missing index for From ... Require ...Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10729: Locations for notation deprecation warningsHugo Herbelin
Reviewed-by: herbelin
2019-09-04Merge PR #10732: Make `Print Rings` and `Print Fields` more reliablethery
Reviewed-by: thery
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
2019-09-04Remove commented-out codeMaxime Dénès
2019-09-04Make `Print Rings` and `Print Fields` reliableMaxime Dénès
Previously, they were using a map that was different from the one used by the real lookup, leading to confusing information (number of instances could be wrong, etc).
2019-09-03Add lemmas directly relating List.nth and List.nth_errorOliver Nash
2019-09-03Remove redundant parameter in List.concat_filter_mapOliver Nash
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-09-03Locations for notation deprecation warningsMaxime Dénès
2019-09-03Merge PR #10651: New lemmas for List.vHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2019-09-03Apply suggestions from code reviewOliver Nash
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-09-03New lemmas for List.vOliver Nash
* filter_app (moved from MSets/MSetRBT.v) * filter_map * filter_ext_in * ext_in_filter * filter_ext_in_iff * filter_ext * concat_filter_map * combine_nil * combine_firstn_l * combine_firstn_r * combine_firstn * nodup_fixed_point
2019-09-02Merge PR #10645: [ci] Update to OCaml 4.08.1Gaëtan Gilbert
Ack-by: Zimmi48 Reviewed-by: vbgl Reviewed-by: SkySkimmer
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
Reviewed-by: gares
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
Reviewed-by: maximedenes
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
Reviewed-by: maximedenes
2019-09-02Merge PR #10716: [funind] Don't export duplicate save function.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: herbelin Ack-by: mattam82 Reviewed-by: ppedrot
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
This is step 1 on removing library state from the lower layers. Here we move library loading to the vernacular layer; few things depend on it: - printers: we add a parameter for those needing to access on-disk data, - coqlib: indeed a few tactics do try to check that a particular library is loaded; this is a tricky part. I've replaced that for a module name check, but indeed this is fully equivalent due to side-effects of `Require`. We may want to think what to do here. A few other minor code movements were needed, but there are self-explanatory.
2019-08-30Adding a critical-bugs entry. Description from Hugo Herbelin.Pierre-Marie Pédrot
2019-08-30Merge PR #10714: Solve universe error with SSR 'rewrite !term'Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
Matthieu Sozeau explained how to fix this.
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-29Merge PR #10693: Create a maintainer team for the contributing process files.Maxime Dénès
Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-08-29[funind] Don't export duplicate save function.Emilio Jesus Gallego Arias
It will take a bit more to clean up the mess with entries in the `indfun` plugin [quite a few PRs in the queue], but thanks to recent refactoring the tricky parts are self-contained now in `gen_principle` so we can remove the duplicated `save` function from the public API.
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ↵Pierre-Marie Pédrot
proof data on top of declare. Reviewed-by: ppedrot
2019-08-29Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify ↵Pierre-Marie Pédrot
exception names Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 11:59:57 +0000