aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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 #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-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
2020-06-19Share the identity instance in pretyping environments.Pierre-Marie Pédrot
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
Instead of costly linear reallocations, we share as much as possible of the prefixes of the various environment subcomponents.
2020-06-18Merge PR #12536: tactics.rst: fix typo — readd `cbv` to title of its sectionThéo Zimmermann
Reviewed-by: jfehrle
2020-06-17[ci] Use a tested branch of PerennialTej Chajed
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
Hope this is enough, also looking at https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
2020-06-17Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` viewCyril Cohen
Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-06-17Merge PR #12506: [toplevel] Annotate tailcall functionsEnrico Tassi
Reviewed-by: maximedenes
2020-06-17Use an efficient data structure for VM compilation indexing.Pierre-Marie Pédrot
2020-06-17Check duplicity of constructor names in an algorithmically efficient way.Pierre-Marie Pédrot
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
Fixes #12529
2020-06-16Use evar clauses instead of meta clauses in Autorewrite hint registration.Pierre-Marie Pédrot
This is barely more meaningful but at least we do not rely on an antiquated API now.
2020-06-16Code simplification in Autorewrite.Pierre-Marie Pédrot
2020-06-16Remove dead code in autorewrite.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:29:59 +0000