aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
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-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.
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
This is in preparation for the next commit which will clean-up the current API flow in `Declare`.
2020-06-26[declare] Move udecl to Info structure.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of deprecated functionsEmilio Jesus Gallego Arias
The previous refactoring in `Declare` to add `CInfo.t` makes this a good moment to clean overlays up w.r.t. deprecation. All cases but one is just a matter of simple renaming, for the other the use of an internal API is replaced by newer API.
2020-06-26[declare] Make ProgramDecl.t abstractEmilio Jesus Gallego Arias
This hides even more internals; we will reduce the API even more shortly.
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
This improves the interface, and allows even more sealing of the API. This is yet work in progress.
2020-06-26[declare] Remove Lemmas moduleEmilio Jesus Gallego Arias
The module is now a stub. We choose to be explicit on the parameters for now, this will improve in next commits with the refactoring of proof / constant information.
2020-06-26[declare] Remove mutual internals from Info.t structure.Emilio Jesus Gallego Arias
We move the advanced proof initialization routine to Declare, and stop exposing implementation internals in `Info.t` constructor.
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface.
2020-06-26[declare] Stronger typing for start_proofEmilio Jesus Gallego Arias
It makes sense to require it to be uni-goal; this also removes some duplication. See the caveat with the handling of `~sign` tho.
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-25Merge PR #12554: Add back fiat-crypto-legacy to the CIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:11:50 +0000