diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-25 22:43:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:28:09 +0100 |
| commit | b1d749e59444f86e40f897c41739168bb1b1b9b3 (patch) | |
| tree | ade1ab73a9c2066302145bb3781a39b5d46b4513 /printing/ppconstr.ml | |
| parent | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (diff) | |
[located] Push inner locations in `reference` to a CAst.t node.
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8854ff898..412a1cbb4 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -213,9 +213,9 @@ let tag_var = tag Tag.variable let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - let pr_reference = function - | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (pr_id id) + let pr_reference = CAst.with_val (function + | Qualid qid -> pr_qualid qid + | Ident id -> tag_var (pr_id id)) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -565,8 +565,8 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,Ident (_,var),us),[t]) - | CApp ((_, {CAst.v = CRef(Ident(_,var),us)}),[t,None]) + | CAppExpl ((None,{v=Ident var},us),[t]) + | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) when Id.equal var Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), |