aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12504: [states] Move States to vernacGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: maximedenes
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-07-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-01Merge PR #12615: [ci] [performance-tests] Use a lighter target.Gaëtan Gilbert
Reviewed-by: JasonGross Reviewed-by: SkySkimmer
2020-07-01Use weak ref to memoize Evarutil.is_ground_envGaëtan Gilbert
2020-07-01Merge PR #12616: [ci] Disable the OCaml 4.12 targetGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-01[ci] Disable the OCaml 4.12 targetEmilio Jesus Gallego Arias
Recent changes in Coqbot plus the unfortunate breakage OCaml upstream has make this too noisy. We will re-enable once https://github.com/ocaml/dune/pull/3585 is accepted upstream.
2020-06-30Cleanup mentions of -as in coqdep usage messageGaëtan Gilbert
2020-06-30[ci] [performance-tests] Use a lighter target.Emilio Jesus Gallego Arias
The current `perf` CI target is quite heavy, failing from out of memory sometimes. We use the target suggested by Jason Gross (<- thanks) in https://github.com/coq/coq/pull/12577#issuecomment-651970064
2020-06-30docs(README.md): Update badge and linksErik Martin-Dorel
* Coq images are not built anymore from a Docker Hub automated build, they are now built from this GitLab CI project: https://gitlab.com/coq-community/docker-coq
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
Now that `Printmods` is above `Declaremods`, we don't need to pass the extra `mod_ops` argument.
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias
We continue to push state layers upwards, in preparation of a functional vernacular interpretation. Now we move `States` and `Printmod` which messes with the global state as to temporarily create envs with modules.
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic ↵Emilio Jesus Gallego Arias
definitions Reviewed-by: ejgallego Reviewed-by: herbelin
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
Apparently the `Timeout` exception is raised by a signal handled, and that can happen when the running thread is a worker manager, rather than the main thread (the one that should be interrupted). Given that the point of these tests is to test *auto and not the STM, we disable async proofs forcibly.
2020-06-29Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-29Adding overlay.Pierre-Marie Pédrot
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.Pierre-Marie Pédrot
2020-06-29Merge PR #12604: Update CAMLDONTLINK in CoqMakefile.inEnrico Tassi
Reviewed-by: gares
2020-06-29Merge PR #12372: [declare] Refactor constant information into a record.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-28Update CAMLDONTLINK in CoqMakefile.inAndres Erbsen
I used SYSMOD from Makefile.build as the ground truth.
2020-06-27Merge PR #12518: [ci] [ocaml] Track OCaml 4.12Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-27Merge PR #12583: [test-suite] Fix dependencies of modules/ filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-26Merge PR #12598: Mention VSCoq with respect to _CoqProjectThéo Zimmermann
Reviewed-by: Zimmi48
2020-06-26Mention VSCoq with respect to _CoqProjectCarl Patenaude-Poulin
2020-06-26[ci] Add overlays for PR #12372Emilio Jesus Gallego Arias
2020-06-26[recLemmas] Nit on naming consistency.Emilio Jesus Gallego Arias
2020-06-26[declare] Return list of declared global in Proof.saveEmilio Jesus Gallego Arias
This is needed in rewriter as to avoid hack; indeed it makes sense to propagate this information to the callers of save.
2020-06-26[declare] Some more cleanup on unused functions after the last commits.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Proof_ending from the public APIEmilio Jesus Gallego Arias
This completes the refactoring [for now] of the core `Declare` interface, and will allow much internal refactoring in the future. In particular, we remove the low-level Proof_ending type, and instead introduce higher-level constructors for the several declare users. Future PRs will change the internal representation of proof handling to better enforce some invariants that should hold for specific proofs.
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
This allows us to remove a large chunk of the internal API, and is the pre-requisite to get rid of [Proof_ending], and even more refactoring on the declare path.
2020-06-26[obligation] Switch to new declare info API.Emilio Jesus Gallego Arias
2020-06-26[declare] Improve logical code orderEmilio Jesus Gallego Arias
Now that the interface has mostly stabilized, we move code around to respect internal dependency order. This will allow us to start sharing more code in the 4 principal cases, and also paves the way for the full merging of obligations and the removal of the Proof_ending type in favor of stronger type abstraction.
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
We unify information about constants so it is shared among all the paths [interactive, NI, obligations]. IMHO the current setup looks pretty good, with information split into a per-constant record `CInfo.t` and variables affecting mutual definitions at once, which live in `Info.t`. Main information outside our `Info` record is `opaque`, which is provided at different moments in several cases. There are a few nits regarding interactive proofs, which will go away in the next commits.
2020-06-26[vernac] Nit refatoring on lemma command interpretationEmilio Jesus Gallego Arias
2020-06-26[declare] Nit on regular lemma init.Emilio Jesus Gallego Arias
2020-06-26[declare] Use Recthm.t in mutual analysis functionsEmilio Jesus Gallego Arias
This removes so ad-hoc tuples, and encapsulates the API a bit. It is a step towards: - Pushing some `to_constr` from the upper layers to the declare code itself [which will remove code duplication, in particular making the interactive / non-interactive path more uniform, and make the API easier to use] - Further refactoring of the constant information, as `Recthm.t` contains almost now what we would call "primitive constant information"; thus we will be able to distinguish next better between mutual declarations and single-constant ones.
2020-06-26[declare] Refactor analysis and construction of mutual lemmasEmilio Jesus Gallego Arias
When declaring a lemma, the code path is quite different depending on whether the lemma is inferred to be a mutually-defined lemma or not. We refactor the code path in declare to reflect that; this will allow to better organize constant information and to reuse the `Recthm.t` type in particular.
2020-06-26[declare] Nit on hook call.Emilio Jesus Gallego Arias
2020-06-26[declare] Nit on interfaceEmilio Jesus Gallego Arias
2020-06-26[declare] Documentation on obligationsEmilio Jesus Gallego Arias
2020-06-26[declare] [compat] Remove exception alias.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Modify logical presentation of declare interfacesEmilio Jesus Gallego Arias
Step towards merging `Info / `CInfo`; the presentation order is now "final" in the sense of that we propose this API for the medium-term.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 04:31:39 +0000