aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-06-25Merge PR #12579: Simplify Clenv APIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-25Merge PR #12580: Remove the catchable-exception related functions.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-25[ci] [ocaml] Track OCaml 4.12Emilio Jesus Gallego Arias
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
This should make the univbinders output test less fragile as it depends less on the global counter (still used for universes from section variables).
2020-06-25Make compute_instance_binders internal to UStateGaëtan Gilbert
2020-06-24[ci] [fiat-crypto-legacy] allow_failure: trueJason Gross
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
Fixes #12582 The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime `plik.v.log` is older than `Nat.vo`. This is circular, and results in `make` considering all of the `modules/` tests out-of-date on any fresh run.
2020-06-24Merge PR #12517: Fix #4459 by improving `par:` error messageEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-06-24Add back fiat-crypto-legacy to the CIJason Gross
This partially reverts commit 35a1cc4f5c708b745a2810a64d220f49eff4beca. (I've not added back the nix things, since I'm not sure what purpose they serve, and I've adjusted the targets slightly.) The CI build should no longer take an enormously long time to start, and fiat-crypto-legacy code is actively being used to track down memory issues in #12487. Additionally, f-c-l revealed a genuine bug in #7825, and so I'd like to keep f-c-l in the CI at least until #7825 is finished. I've been maintaining compatibility of f-c-l with master anyway on the side, in part to continue some performance experiments with it, and expect to continue to do so at least until the end of this calendar year, and it'd be nice for me to get advance warning when a PR is going to break it on master. (It seems reasonable to me to take it off the CI again once I'm no longer maintaining it / collecting data from it, and / or once #7825 is finished.)
2020-06-24Remove the catchable-exception related functions.Pierre-Marie Pédrot
They were deprecated in 8.12.
2020-06-24Simplify Clenv.clenv_pose_metas_as_evars.Pierre-Marie Pédrot
No need to return the list of generated evars, this was never used.
2020-06-24Actually remove internal API from the Clenv mli.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
Having two different modules led to the availability of internal API in the mli.
2020-06-24Remove all uses of clenv_unique_resolver.Pierre-Marie Pédrot
All calls to this function are now factorized through Clenvtac.res_pf.
2020-06-24Remove dead code in branch_args.Pierre-Marie Pédrot
2020-06-24Merge PR #12550: Fix configure usage in .opamEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: maximedenes
2020-06-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
Reviewed-by: mattam82
2020-06-24Revert "[opam] Don't disable native compute in opam.dev file"Gaëtan Gilbert
This reverts commit b35030760cadd96a968e04f3cd026f4abdc0331c.
2020-06-24Merge PR #12577: [ci] Add coq-community/coq-performance-testsGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-23[ci] Add coq-community/coq-performance-testsJason Gross
It's tested on the bench, so might as well test it on the CI. Hopefully it's not too memory-heavy. (It should only take a couple of minutes, time-wise.)
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
Fixes #12571.
2020-06-23Merge PR #12562: CoqIDE: accept to open files with invalid namesMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: SkySkimmer
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
Reviewed-by: gares Reviewed-by: maximedenes
2020-06-23Fix #4459 by improving `par:` error messageMaxime Dénès
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
Reviewed-by: fajb
2020-06-23Merge PR #8796: Elementary properties about IZR for generic useGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-23CoqIDE: fix lexing of UTF-8 in quotations like constr:()James Lottes
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-23Use the unification result for eauto's eapply.Pierre-Marie Pédrot
Instead of dropping the unification result and calling simple eapply with the original term, we simply use the same code path as auto and typeclass eauto, i.e. reuse the clenv for refinement.
2020-06-22Merge PR #12520: Cleanup the autorewrite implementationHugo Herbelin
Reviewed-by: herbelin
2020-06-22Elementary properties about IZR for generic use.Hugo Herbelin
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential ↵Gaëtan Gilbert
variables in goals Reviewed-by: SkySkimmer
2020-06-22Merge PR #12555: Add test-suite/redirect_test.out file to .gitignoreGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-22Merge PR #12546: [ci] Use a tested branch of PerennialEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
2020-06-21Merge PR #12505: Cleanup the Hints APIHugo Herbelin
Reviewed-by: herbelin
2020-06-21Merge PR #12559: Add index for coqdoc.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-06-21Add index for coqdoc.Théo Zimmermann
Fixes #12545.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 08:22:10 +0000