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.

Sign up for GitHub

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

Jump to bottom

Uniformize the name of the Ltac2 boolean equality function. #14128

Merged
merged 1 commit into from
Apr 22, 2021
Merged

Uniformize the name of the Ltac2 boolean equality function. #14128

merged 1 commit into from
Apr 22, 2021

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented Apr 17, 2021 •
edited
Loading

All other equality functions are called "equal" but this one was called "eq". We add a deprecated alias for backward compatibility.

@ppedrot ppedrot requested a review from a team as a code owner April 17, 2021 18:10
@ppedrot
Uniformize the name of the Ltac2 boolean equality function.
e27fdd1 
All other equality functions are called "equal" but this one was called "eq".
We add a deprecated alias for backward compatibility.
@ppedrot ppedrot added this to the 8.14+rc1 milestone Apr 17, 2021
@ppedrot ppedrot added the kind: fix This fixes a bug or incorrect documentation. label Apr 17, 2021
@ppedrot
Copy link
Member Author

ppedrot commented Apr 22, 2021

This is fairly trivial and needs an assignee.

@JasonGross JasonGross self-assigned this Apr 22, 2021
@JasonGross JasonGross added part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. part: standard library The standard library stdlib. labels Apr 22, 2021
@JasonGross
Copy link
Member

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d758cc5 into coq:master Apr 22, 2021
@ppedrot ppedrot deleted the ltac2-bool-equal-rename branch April 22, 2021 11:55
@MSoegtropIMC
Copy link
Contributor

A note for completeness: in OCaml - to which Ltac2 shouldn't be needlessly incompatible - the Bool equality function is also called equal. See (https://ocaml.org/api/Bool.html).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JasonGross JasonGross JasonGross approved these changes

Assignees

@JasonGross JasonGross

Labels
kind: fix This fixes a bug or incorrect documentation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. part: standard library The standard library stdlib.
Projects
None yet
Milestone
8.14+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@ppedrot @JasonGross @MSoegtropIMC