aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-08Merge PR #11042: The "univ poly can capture global univs" checker side bug ↵Théo Zimmermann
is fixed Reviewed-by: Zimmi48
2019-11-07Do not rely on the user settings but on the actual window size. (Fixes #10956)Guillaume Melquiond
This should fix the issue when creating new session panes. The initial session panes, however, might still be wrongly sized, as we do not yet know, at the time they are created, if the window manager will respect the user settings fixing the window size.
2019-11-07Do not include final stops in queries. (Fixes #11058)Guillaume Melquiond
The bug was introduced by #10063, which eagerly added dots to identifier without considering whether they are related to the identifier. Along the way, this commit also prevents primes and digits from being added as initial characters of identifiers. This works for both word selection and queries. Note that there is still a small issue with word selection, when the current word starts with a digit. Indeed, when double-clicking, GTK will already have extended the selection to it, so we have no way of preventing the digit from being part of the selection. This commit also fixes the unusual calling convention of Gtk_parsing.end_words.
2019-11-07The "univ poly can capture global univs" checker side bug is fixedGaëtan Gilbert
(by the checker refactor AFAICT) + fix commit for the coqtop side fix (it got rebased at some point) Close #10705
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ↵Pierre-Marie Pédrot
a module Reviewed-by: ppedrot
2019-11-07Merge PR #11059: Swap parsing precedence of `::` and `,` ; Fix #10116Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-06Merge PR #11038: fix(*.opam): Add missing version "dev"Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-06Merge PR #11041: Cite POPL19 SProp paperThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-06Merge PR #11051: elpi 1.8Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-11-05Fixing test-suiteKenji Maillard
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
Reduction.whd_all does not commute with to_constr.
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
This probably does not work well in general, and specifically avoids an anomaly fixing https://github.com/coq/coq/issues/10060
2019-11-05overlayEnrico Tassi
2019-11-05elpi 1.8Enrico Tassi
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
2019-11-04Prevent redefinition of Ltac2 types; fix #10097Kenji Maillard
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
Close #10242
2019-11-04fix(*.opam): Add missing versionErik Martin-Dorel
"dev" was not implied, and this can cause the following issues: --8<---------------cut here---------------start------------->8--- $ docker run --rm -it coqorg/base:latest coq@…:~$ opam update coq@…:~$ git clone https://github.com/coq/coq.git Cloning into 'coq'... coq@…:~$ cd coq coq@…:~/coq$ opam pin add -n -k path coq . [coq.8.10.1] synchronised from file:///home/coq/coq coq is now pinned to file:///home/coq/coq (version 8.10.1) # issue 1. opam picks the first version he finds for coq from repos… coq@…:~/coq$ mv coq.opam foo.opam coq@…:~/coq$ opam pin add -n -k path foo . Package foo does not exist, create as a NEW package? [Y/n] y [foo.~dev] synchronised from file:///home/coq/coq foo is now pinned to file:///home/coq/coq (version ~dev) # issue 2. if none is found, opam sticks to some "~dev" version… --8<---------------cut here---------------end--------------->8---
2019-11-03Merge PR #10958: Elan → Stratego in documentation of `rewrite_strat`.Théo Zimmermann
Reviewed-by: Zimmi48
2019-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
@eelcovisser told me that the strategies in Luttik and Visser 97 were inspired by Elan, but they are not part of Elan. They are part of the Stratego language.
2019-11-02Merge PR #11007: [classes] Some refactoring on proof save preparation.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-01Merge PR #11028: Update the deprecation doc of `Shrink Obligations`Clément Pit-Claudel
2019-11-01Merge PR #10647: Expose universe processing in comInductive.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵Enrico Tassi
relation Reviewed-by: gares
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
Now it uses `.. deprecated` like all the other deprecation notices in the manual.
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
2019-11-01minor cleanup of anonymous functionsGaëtan Gilbert
2019-11-01Expose universe processing in comInductive.Jan-Oliver Kaiser
2019-11-01Merge PR #8642: Compiled interfaces with -vos and -vok optionsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-11-01Merge PR #11019: enforcing Ltac2 constructor name are uppercasedPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-11-01enforcing Ltac2 cosntructors name are uppercase in open typesKenji Maillard
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01Teach coq_dune about the empty .vos produced by coqcGaëtan Gilbert
Without this the next dune command after build a vo will wipe out the vos, breaking interactive users. Also this means dune installs the .vos files.
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01[make] install .vos along with .voEnrico Tassi
2019-11-01fix installation of vos files in coq Makefilecharguer
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall ↵charguer
that the generation of a .vo files induces the creation of an empty .vos file.)
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01Changelog entryMaxime Dénès
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file.
2019-11-01Merge PR #11015: [Nix] Update reference to nixpkgsThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-01docs(gallina-extensions.rst): Say more on float literals extractionErik Martin-Dorel
2019-11-01Communicate CFLAGS to dunePierre Roux
2019-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
(as suggested by @silene)
2019-11-01Makefile.build: Fix rules of bin/votour{,.byte}Erik Martin-Dorel
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 12:21:51 +0000