Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

switching long suffixes to short suffixes #473

Merged
merged 1 commit into from Apr 9, 2020

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Apr 7, 2020

  • odd_add -> oddD
  • odd_sub -> oddB
  • take_addn -> takeD
  • rot_addn -> rotD
  • nseq_addn -> nseqD
Motivation for this change

fixes #359

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    - [ ] added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

@affeldt-aist affeldt-aist changed the title - switching long suffixes to short suffixes switching long suffixes to short suffixes Apr 7, 2020
@CohenCyril
Copy link
Member

@affeldt-aist looks like fourcolour needs an overlay

@affeldt-aist affeldt-aist force-pushed the long_short_suffixes branch 6 times, most recently from d42b4a6 to eaae7b8 Compare April 8, 2020 00:04
@pi8027
Copy link
Member

pi8027 commented Apr 8, 2020

Hello. Shouldn't we use the deprecation facility rather than having overlays?

(* deprecate old new == new, but warning that old is deprecated and new *)
(* should be used instead. *)
(* --> Usage: Notation old := (deprecate old new) (only parsing). *)
(* --> Caveat: deprecate old new only inherits new's maximal implicits; *)
(* on-demand implicits should be added after : (deprecate old new _). *)
(* --> Caveat 2: if premises or conclusions need to be adjusted, of for *)
(* non-prenex implicits, use the idiom: *)
(* Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) *)
(* _ _ ... _) (only printing). *)
(* where all the implicit a_i's occur first, and correspond to the *)
(* trailing _'s, making sure deprecate old new is fully applied and *)
(* there are _no implicits_ inside the (fun .. => ..) expression. This *)
(* is to avoid triggering a bug in SSReflect elaboration that is *)
(* triggered by such evars under binders. *)

mathcomp/ssreflect/seq.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

Hello. Shouldn't we use the deprecation facility rather than having overlays?

Indeed. Will do.

  + `odd_add` -> `oddD`
  + `odd_sub` -> `oddB`
  + `take_addn` -> `takeD`
  + `rot_addn` -> `rotD`
  + `nseq_addn` -> `nseqD`

fixes math-comp#359
@affeldt-aist affeldt-aist merged commit dc1ea50 into math-comp:master Apr 9, 2020
@affeldt-aist affeldt-aist deleted the long_short_suffixes branch April 17, 2020 15:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Theorem names in ssrnat (switching long suffixes to short suffixes)
4 participants