aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-12Merge PR #11092: [dune] Have only one rule calling configureEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: gares Reviewed-by: ppedrot
2019-11-11Have only one dune rule calling configurePierre Roux
2019-11-11Merge PR #11032: Run update-compat script with --release option.Pierre-Marie Pédrot
Reviewed-by: JasonGross Ack-by: ppedrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-09Merge PR #11017: Make [Proof_global.closed_proof_output] opaquePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
This means return_proof is the only place where it can be produced. We need to change the stm a bit as it keeps a pointer to a [closed_proof_output] to join and to check if it failed, and it needs a way to create a dummy in 1 case. I'm not sure if this works correctly though, how to test? We also inline the used bits of [return_proof ~allow_partial:true] in [save_lemma_admitted] to get [Proof using] info. We could alternatively expose the [closed_proof_output -> constr list] projection. I think the code is easier to understand this way though, as we don't have to read [return_proof] and figure out that the side effect manipulation is ignored etc. Note that the "this will warn" comment was outdated since 73daf37ccc7a44cd29c9b67405111756c75cb26a
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-08Merge PR #11069: Do not include final stops in queries. (Fixes #11058)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
Reviewed-by: Zimmi48
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 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:37:30 +0000