aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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
2020-06-16make the linter happyEnrico Tassi
2020-06-15Merge PR #12509: updated ci for unicoqThéo Zimmermann
Reviewed-by: Zimmi48
2020-06-15updated ci for unicoqbeta
2020-06-15Merge PR #11906: [micromega] native support for boolean operatorsMaxime Dénès
Reviewed-by: maximedenes Reviewed-by: pi8027 Reviewed-by: vbgl
2020-06-15[ssr] fix env handling in error message (fix #12507)Enrico Tassi
2020-06-15[ssr] remove catch allEnrico Tassi
2020-06-15Merge PR #12494: [dev/ci/nix] Support for building the Gappa plugin.Vincent Laporte
Reviewed-by: vbgl
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-14Update theories/micromega/ZifyBool.vFrédéric Besson
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:05:51 +0000