aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Collapse)Author
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
fix unexpectedly broken MSetGenTree.v add changelog entry
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
Reviewed-by: anton-trunov
2021-01-29add results on count_occOlivier Laurent
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-08Modify Lists/SetoidList.v to compile with -mangle-namesJasper Hugunin
I used `match goal` a lot to access hypotheses without knowing their name.
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-09-16Modify Lists/List.v to compile with -mangle-namesJasper Hugunin
2020-09-07Add iff variants for other list lemmasEdward Wang
2020-09-07Add iff variant for app_inj_tailEdward Wang
The lemma is true in the other direction and can be useful in proofs.
2020-08-12Additional statements about List.repeatOlivier Laurent
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-04add incl_Forall_in_iffOlivier Laurent
2020-05-04strenghten nth_extOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-04-30Symmetry in conclusions of List.map_eq_*Olivier Laurent
allow simplified iterated applications
2020-04-19remove useless hypothesis in NoDup_Permutation_bisOlivier Laurent
(thanks to new NoDup_incl_NoDup)
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-05apply suggestions of @anton-trunovOlivier Laurent
2020-01-05clean some indentationsOlivier Laurent
2019-12-06additional statements on flat_mapOlivier Laurent
2019-12-06additional statements on map and ForallOlivier Laurent
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
2019-12-06integration of list_sum and list_maxOlivier Laurent
2019-12-06integration of statements for repeatOlivier Laurent
2019-12-06integration of statements for NoDupOlivier Laurent
2019-12-06integration of additional statements for inclOlivier Laurent
2019-12-06integration of statements for removeOlivier Laurent
2019-12-06integration of statements for InOlivier Laurent
2019-12-06integration of statements for inclOlivier Laurent
2019-12-06integration of statements for revOlivier Laurent
2019-12-06integration of statements for concat and flat_mapOlivier Laurent
2019-12-06integration of statements for seqOlivier Laurent
2019-12-06integration of statements related to last elementOlivier Laurent
2019-12-06integration of Exists_or and Forall_andOlivier Laurent
2019-12-06redundancy between skipn_node and skipn_allOlivier Laurent
2019-09-03Add lemmas directly relating List.nth and List.nth_errorOliver Nash
2019-09-03Remove redundant parameter in List.concat_filter_mapOliver Nash
2019-09-03New lemmas for List.vOliver Nash
* filter_app (moved from MSets/MSetRBT.v) * filter_map * filter_ext_in * ext_in_filter * filter_ext_in_iff * filter_ext * concat_filter_map * combine_nil * combine_firstn_l * combine_firstn_r * combine_firstn * nodup_fixed_point
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
This could be Prop (for compat with usual Coq), Set (for HoTT), or actually an arbitrary "i". Take lower bound of universes into account in pretyping/engine Reinstate proper elaboration of SProp <= l constraints: replacing is_small with equality with lbound is _not_ semantics preserving! lbound = Set Elaborate template polymorphic inductives with lower bound Prop This will make more constraints explicit Check univ constraints with Prop as lower bound for template inductives Restrict template polymorphic universes to those not bounded from below Fixes #9294 fix suggested by Matthieu Try second fix suggested by Matthieu Take care of modifying elaboration for record declarations as well. Rebase and export functions for debug Remove exported functions used while debugging Add a new typing flag "check_template" and option "-no-template-checl" This parameterizes the new criterion on template polymorphic inductives to allow bypassing it (necessary for backward compatibility). Update checker to the new typing flags structure Switch on the new template_check flag to allow old unsafe behavior in indTyping. This is the only change of code really impacting the kernel, together with the commit implementing unbounded from below and parameterization by the lower bound on universes. Add deprecated option `Unset Template Check` allowing to make proof scripts work with both 8.9 and 8.10 for a while Fix `Template Check` option name and test it Add `Unset Template Check` to Coq89.v Cooking of inductives and template-check tests Cleanup test-suite file for template check / universes(template) flags cookind tests Move test of `Unset Template Check` to the failure/ dir, but comment it for now Template test-suite test explanation Overlays for PR 9918 Overlay for paramcoq Add overlay for fiat_parsers (-no-template-check) Add overlay for fiat_crypto_legacy Update fiat-crypto legacy overlay Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made. Remove overlay that should no longer be necessary The setting in the compat file should handle it Remove now-merged fiat-crypto-legacy overlay Update `Print Assumptions` to reflect the typing flag for template checking Fix About and Print Assumptions for template poly, giving info on which variables are actually polymorphic Fix pretty printing to print global universe levels properly Fix printing of template polymorphic universes Fix pretty printing for template polymorphism on no universe Fix interaction of template check and universes(template) flag Fix indTyping to really check if there is any point in polymorphism: the conclusion sort should be parameterized over at least one local universe Indtyping fixes for template polymorphic Props Allow explicit template polymorphism again Adapt to new indTyping interface Handle the case of template-polymorphic on no universes correctly (morally Type0m univ represented as Prop). Fix check of meaningfullness of template polymorphism in the kernel. It is now done w.r.t the min_univ, the minimal universe inferred for the inductive/record type, independently of the user-written annotation which must only be larger than min_univ. This preserves compatibility with UniMath and template-polymorphism as it has been implemented up-to now. Comment on identity non-template-polymorphism Remove incorrect universes(template) attributes from ssr simpl_fun can be meaningfully template-poly, as well as pred_key (although the use is debatable: it could just as well be in Prop). Move `fun_of_simpl` coercion declaration out of section to respect uniform inheritance Remove incorrect uses of #[universes(template)] from the stdlib Extraction of micromega changes due to moving an ind decl out of a section Remove incorrect uses of #[universes(template)] from plugins Fix test-suite files, removing incorrect #[universes(template)] attributes Remove incorrect #[universes(template)] attributes in test-suite Fix test-suite Remove overlays as they have been merged upstream.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
sometimes, to use "intros [= ...]" rather than things like "intros H; injection H as [= ...]". Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-23Fixing typos - Part 3JPR
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
This is intended to be separate from handling of implicit binders. The remaining uses of declare_manual_implicits satisfy a lot of assertions, giving the possibility of simplifying the interface in the future. Two disabled warnings are added for things that currently pass silently. Currently only Mtac passes non-maximal implicits to declare_manual_implicits with the force-usage flag set. When implicit arguments don't have to be named, should move Mtac over to set_implicits.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:00:00 +0000