aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-24[ci] [fiat-crypto-legacy] allow_failure: trueJason Gross
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-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-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.
2020-06-21Add a generated file to .gitignoreJason Gross
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-20Merge PR #12407: Fix #12406: fix Coq type error in dependent induction's LtacAnton Trunov
Reviewed-by: anton-trunov
2020-06-19Merge PR #12531: Fast inductive compilationGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-19Merge PR #12502: Preserve sharing in evar instancesGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2020-06-19Add overlays.Pierre-Marie Pédrot
2020-06-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
It is only used for this kind of hints, never for Extern / Unfold.
2020-06-19Wrap the content of full hints into a record.Pierre-Marie Pédrot
2020-06-19Remove access to hint section variables.Pierre-Marie Pédrot
The only use was seemingly a bug introduced in 0aec9033a by an accidental variable capture. There is indeed no reason that the set of variables of a hint corresponds to the one of the current environment.
2020-06-19Opacify the type of hint metadata.Pierre-Marie Pédrot
2020-06-19Remove dead code in the Hints API.Pierre-Marie Pédrot
2020-06-19Do not export Hints.make_extern.Pierre-Marie Pédrot
2020-06-19Do not export flags in Hints.make_resolves.Pierre-Marie Pédrot
They are always the same.
2020-06-19Do not be verbose when declaring subclass hints.Pierre-Marie Pédrot
There is no point in warning about eauto being the only one able to use those hints, since they will be used by typeclass_eauto instead. It was probably an oversight introduced quite a long time ago.
2020-06-19Factorize hint flags in Class_tatcis.make_make_resolve_hyp.Pierre-Marie Pédrot
They were always instantiated with the triple (true, false, false).
2020-06-19Try to preserve more sharing in nf_evars_and_universes_opt_subst.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:05:32 +0000