[hover] Fix universe printing in hover. #839
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ejgallego
force-pushed
the
fix_hover_print_ind
branch
from
ad90b3f
to
293591f
Compare
|
How does the new version print? |
ejgallego
force-pushed
the
fix_hover_print_ind
branch
from
293591f
to
79d3065
Compare
Alizter
reviewed
Sep 28, 2024
controller/rq_hover.ml
Outdated
| @@ -128,10 +162,11 @@ let pp_file fmt = function | |||
| | Some file -> Format.fprintf fmt " - **in file**: `%s`" file | |||
|
|
|||
| let pp_typ id = function | |||
| | Def (typ, cr, file) -> | |||
| | Def (typ, param, cr, file) -> | |||
There was a problem hiding this comment.
Probably best to call this sort_param or something.
foo@{u u0 u1} (M : Type@{u}) : Type@{u0} -> Type@{max(u,u1+1)} |
Alizter
reviewed
Sep 28, 2024
Alizter
approved these changes
Sep 28, 2024
Our code was incomplete. The API here could be really improved Coq-side. About is too verbose for hover, hence our code. We could opt for the version in `prettyp.ml` tho. Fixes #835
ejgallego
force-pushed
the
fix_hover_print_ind
branch
from
79d3065
to
0ae1e56
Compare
Alizter
reviewed
Sep 28, 2024
| ; full_path : Names.Constant.t option | ||
| (** full path of the constant, if any, for example | ||
| [Stdlib.Lists.map] *) | ||
| ; file : string option (** filename where the constant is located *) |
There was a problem hiding this comment.
Do we have access to the location too? (The one goto definition uses). Not relevant for this PR, but it might be useful to include.
There was a problem hiding this comment.
We could, but not sure line number is relevant here, the client can indeed issue the corresponding specific request for location.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Our code was incomplete. The API here could be really improved Coq-side. About is too verbose for hover, hence our code. We could opt for the version in
prettyp.mltho.Fixes #835