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

Annotating terms #25

Merged
merged 2 commits into from
Sep 23, 2019
Merged

Annotating terms #25

merged 2 commits into from
Sep 23, 2019

Conversation

teofr
Copy link
Contributor

@teofr teofr commented Sep 18, 2019

This PR introduces a simple wrapper around Term, this will allow us to have extra information on them.

For now this doesn't add any extra information.
Probably the first bit of information will be source file location, which should improve greatly a coming call trace.

@teofr teofr requested review from mboes and aspiwack September 18, 2019 09:44
@teofr teofr self-assigned this Sep 18, 2019
@teofr teofr force-pushed the teofr/fixing-operation branch 2 times, most recently from 4d79857 to 501d0be Compare September 23, 2019 08:17
this will allow us to have information over them, think location
@teofr teofr force-pushed the teofr/annotating-terms branch from 5ed8118 to 26d6739 Compare September 23, 2019 08:30
@teofr teofr changed the base branch from teofr/fixing-operation to master September 23, 2019 08:31
@teofr
Copy link
Contributor Author

teofr commented Sep 23, 2019

Rebased.

@teofr teofr merged commit 8574885 into master Sep 23, 2019
@teofr teofr deleted the teofr/annotating-terms branch September 23, 2019 08:46
@mboes mboes unassigned teofr Mar 20, 2020
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.

2 participants