aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-04Improve language.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-09-18Fix syntax of reduction tactics when listing qualid to reduce or not.Théo Zimmermann
2019-09-17Merge PR #10476: Remove library-specific code for `Import`.Enrico Tassi
Reviewed-by: gares Reviewed-by: ppedrot
2019-09-17Add changelog entryMaxime Dénès
2019-09-17Overlay for VSTMaxime Dénès
2019-09-16Optimize multiple importsMaxime Dénès
2019-09-16Optimize `Include`d `Export`sMaxime Dénès
2019-09-16Turn `module_objects` into a recordMaxime Dénès
2019-09-16Add SF overlayMaxime Dénès
2019-09-16Optimize module ExportsMaxime Dénès
This should compensate the removal of the library-level optimization, while maintaining correct behavior.
2019-09-16Do not cache objects when importing modulesMaxime Dénès
They have been already cached at loading time.
2019-09-16Specialize `ImportObject` to `Export`Maxime Dénès
`Import` does not actually need to register an object, only `Export` does. So we specialize and rename the object into `ExportObject`.
2019-09-16`do_modtype` -> `load_modtype`Maxime Dénès
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
Libraries are now handled like other modules.
2019-09-13Merge PR #10748: Hack for fixing #10578: handle between the three main ↵Pierre-Marie Pédrot
CoqIDE windows not always set at the expected position Reviewed-by: ppedrot Reviewed-by: silene
2019-09-13Hack for fixing #10578 (wrong initial handle position separating main windows).Hugo Herbelin
G. Melquiond noticed that the size_allocate event is emitted in the Layout step of the Events-Update-Layout-Paint gtk+ loop so that it is actually processed only when a further event arrived. In some circonstances, this next event has to be an action from the user. So, in some circonstances, at initialization of Coqide, the handle, whose positioning was precisely governed by the size_allocate event, was only set at its expected position after a first action of the user. Before this first action of the user, the handle separating the buffer and the pair of goal and message windows, as well as the handle separating the goal window and the message window were located in the leftmost uppermost corner, which gave an impression of non-usability of CoqIDE. To prevent this, we early set the position of the handle at an estimated value depending on the width and height of the whole coqide windows in the preferences. (Also removing a previous temporary setting of the handle position to - strangely - value 1 but this was anyway overwritten by the size_allocate event.)
2019-09-12Merge PR #10753: Release notes for 8.10+beta3.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-11Merge PR #8567: More general support for installation of coqide keysPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: ppedrot
2019-09-10Merge PR #10742: Switch maintenance of `ring` to a teamThéo Zimmermann
Reviewed-by: Zimmi48
2019-09-10Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.Hugo Herbelin
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-10CoqIDE: removing option contextual menu on goal, inactive since 2da5db43c.Hugo Herbelin
2019-09-10Moving a standard string function (is_prefix) from Minilib to CString.Hugo Herbelin
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:53:27 +0000