aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-16Merge PR #10345: Fix #10339: Anomaly in Ltac2.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-16Merge PR #10327: Fix bug #5710Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-06-16Merge PR #10355: [funind] Untabify; necessary to ease the review of ↵Pierre-Marie Pédrot
subsequent work. Reviewed-by: maximedenes
2019-06-15Merge PR #10040: Install byte version of coqidetop.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-15[dune] Install .byte version of coqidetop like for coqtop.Théo Zimmermann
2019-06-15Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-15Rename expr and tacexpr tokens into ltac_expr token family.Théo Zimmermann
This allows to refer to them from other part of the manual without any ambiguity.
2019-06-14Merge PR #10376: Add a comment documenting what fontsupport.py is.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-14Add a comment documenting what fontsupport.py is.Théo Zimmermann
2019-06-14Merge PR #10322: Update changes.rst as a follow-up to #9743Théo Zimmermann
Reviewed-by: Zimmi48
2019-06-13Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-13Merge PR #10373: Add missing changelog entry for #10360.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-13Integrate 8.9.0 and 8.9.1 changelog entries.Théo Zimmermann
From the CHANGES file in branch v8.9.
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
Ack-by: ejgallego Reviewed-by: gares
2019-06-13Merge PR #10360: Resolve #9885 CoqIDE does not work on WindowsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: vbgl
2019-06-12Merge PR #10310: Fix #10283: clearer dependency documentation for building ↵Clément Pit-Claudel
CoqIDE. Reviewed-by: cpitclaudel Reviewed-by: ejgallego
2019-06-12[funind] Untabify; necessary to ease the review of subsequent work.Emilio Jesus Gallego Arias
2019-06-12Merge PR #10358: [docker] update elpi to 1.3.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-06-12Merge PR #10329: Update changelog for 10302 and 10305Théo Zimmermann
Reviewed-by: Zimmi48
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic ↵Théo Zimmermann
definitions Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ggonthier Reviewed-by: herbelin
2019-06-12Merge PR #10334: Remove the side-effect role from the kernel.Enrico Tassi
Reviewed-by: gares
2019-06-11overlayEnrico Tassi
2019-06-11Adding an overlay for Equations.Pierre-Marie Pédrot
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
We move the role data into the evarmap instead.
2019-06-11Merge PR #10354: [ci] [fiat-crypto] Enable more targets on Coq CIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-11Resolve #9885 CoqIDE does not work on WindowsMichael Soegtrop
- Switch gtksourceview to 3.24.11 - Add appropriate set of icons and some other files GTK3 requires - Add fix for ocamldebug so that this can be debugged
2019-06-11Overlays for 10319Gaëtan Gilbert
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
The stm.ml changes show that for the other classifications either the vernac_when was ignored, or there was an assert on it forcing it to be Now or Later depending on the vernac_type. One may also note that the classification used in top_printers `VtQuery,VtNow` would have failed those asserts...
2019-06-11update elpi to 1.3.1Enrico Tassi
2019-06-10[ci] [fiat-crypto] Enable more targets on Coq CIJason Gross
Closes #10353 May be blocked on #10352
2019-06-10Merge PR #9566: [proof] Move proofs that have an associated constant to `Lemmas`Pierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-06-09Merge PR #10325: Fix panel behavior as requested by #10292Pierre-Marie Pédrot
2019-06-09[ci] Overlays for move_termination_routine_outEmilio Jesus Gallego Arias
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
We rename modify to map [more in line with the rest of the system] and make the endline function specific, as it is only used in one case.
2019-06-09[save_proof] Make terminator API internal.Emilio Jesus Gallego Arias
We refactor the terminator API to make it more internal. Indeed we remove `set_terminator` and `get_terminator` is only there due to access to internals in the STM `save_proof` path by the infamous `?proof` parameter. After this only 2 non-standard terminators remain: obligations and derive. We will refactor those in next PRs.
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
The main idea of this PR is to distinguish the types of "proof object" `Proof_global.t` and the type of "proof object associated to a constant, the new `Lemmas.t`. This way, we can move the terminator setup to the higher layer in `vernac`, which is the one that really knows about constants, paving the way for further simplification and in particular for a unified handling of constant saving by removal of the control inversion here. Terminators are now internal to `Lemmas`, as it is the only part of the code applying them. As a consequence, proof nesting is now handled by `Lemmas`, and `Proof_global.t` is just a single `Proof.t` plus some environmental meta-data. We are also enable considerable simplification in a future PR, as this patch makes `Proof.t` and `Proof_global.t` essentially the same, so we should expect to handle them under a unified interface.
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
Reviewed-by: aspiwack Ack-by: ejgallego Reviewed-by: ppedrot
2019-06-09Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint jobEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the ↵Emilio Jesus Gallego Arias
vernac syntax Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: herbelin
2019-06-08Merge PR #10318: Test goal range in "only" selectorsPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-08Merge PR #10263: [proofs] Remove unused API [detected by coverage]Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
We use a user-facing wrapper instead of a low-level function raising internal exceptions.
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
Formerly, knowing if a declaration was to be discharged, to be global but invisible at import, or to be global but visible at import was obtained by combining the parser-level information (i.e. use of Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use of Local vs Global) with the result of testing whether there were open sections. We change the meaning of the Discharge flag: it does not tell anymore that it was syntactically a Variable/Hypothesis/Let, but tells the expected semantics of the declaration (issuing a warning in the parser-to-interpreter step if the semantics is not the one suggested by the syntax). In particular, the interpretation/command engine becomes independent of the parser. The new "semantic" type is: type import_status = ImportDefaultBehavior | ImportNeedQualified type locality = Discharge | Global of import_status In the process, we found a couple of inconsistencies in the treatment of the locality status. See bug #8722 and test file LocalDefinition.v.
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
This is to avoid depending on the combination "Discharge" + no opened section to trigger an automatic declaration of instance.
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
I don't know what goal_selector.v was supposed to test but CI says nobody relied on it.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:21:06 +0000