From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 25 Feb 2018 22:43:42 +0100 Subject: [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. --- printing/ppconstr.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'printing/ppconstr.ml') 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 ".."), -- cgit v1.2.3