8000 [vernac] [minor] Move print effects to top-level caller. by ejgallego · Pull Request #6702 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

[vernac] [minor] Move print effects to top-level caller. #6702

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
Merged
merged 5 commits into from
Feb 13, 2018
Merged

[vernac] [minor] Move print effects to top-level caller. #6702

merged 5 commits into from
Feb 13, 2018

Conversation

ejgallego
Copy link
Member
@ejgallego ejgallego commented Feb 6, 2018 •
edited
Loading

We remove many individual calls to msg_notice in the print
vernacular dispatcher in favor of a single, top-level call.

This is a minor refactoring but will help in handling Print Foo more uniformly.

@Zimmi48 Zimmi48 added the kind: cleanup Code removal, deprecation, refactorings, etc. label Feb 6, 2018
@Zimmi48 Zimmi48 added this to the 8.8 milestone Feb 6, 2018
@ejgallego ejgallego force-pushed the vernac+print_foo branch 2 times, most recently from 96e88a2 to 3b69345 Compare February 6, 2018 20:38
@Zimmi48 Zimmi48 added the needs: merge of dependency This PR depends on another PR being merged first. label Feb 7, 2018
@ejgallego
[nativecomp] Remove ad-hoc handling of Dynlink exception.
250dc1f 
Instead, we properly register a printer for such exception and update
the code.
@ejgallego
[error] Replace msg_error by a proper exception.
33789b2 
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.

As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
@ejgallego
[vernac] [minor] Move print effects to top-level caller.
dcd2cd3 
We remove many individual calls to `msg_notice` in the print
vernacular dispatcher in favor of a single, top-level calls.

This is a minor refactoring but will help in handling `Print Foo` more uniformly.
@ejgallego
[nit] Remove some unnecessary global open Feedback
79bb4a6
@ejgallego
[vernac] Fix outdated comment.
c0e99b4
@ejgallego ejgallego removed the needs: merge of dependency This PR depends on another PR being merged first. label Feb 12, 2018
@maximedenes maximedenes merged commit c0e99b4 into rocq-prover:master Feb 13, 2018
maximedenes added a commit that referenced this pull request Feb 13, 2018
@maximedenes
Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.
19d4ba5
@ejgallego ejgallego deleted the vernac+print_foo branch February 13, 2018 17:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Milestone
8.8+beta1
Development

Successfully merging this pull request may close these issues.
3 participants
@ejgallego @maximedenes @Zimmi48
0