aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
Now that we place imperative module declaration on top of module interpretation we can remove the abstraction layer used in `Declaremods`, so the `interp_modast` parameter goes away. Improvement suggested by Gaëtan Gilbert.
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
We move `Declaremods` to the vernac layer as it implement vernac-specific logic to manipulate modules which moreover is highly imperative. This forces code [such as printing] to manipulate the _global imperative_ state which is a bit fishy. The key improvement in this PR is that now `Global` is not used anymore in `library`, so we can proceed to move it upwards. This move is a follow-up of #10562 and a step towards moving `Global` upper, likely to `interp` in the short term.
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot Ack-by: vbgl
2019-09-17Merge PR #10738: update elpi to 1.7Gaëtan Gilbert
Reviewed-by: SkySkimmer
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-16Re-implementation of zifyFrédéric Besson
The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:46:54 +0000