diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 10 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 2 | ||||
| -rw-r--r-- | printing/pputils.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 6 | ||||
| -rw-r--r-- | printing/printer.ml | 6 |
5 files changed, 13 insertions, 13 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 117e1900d..fddd54a9f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -145,9 +145,9 @@ let tag_var = tag Tag.variable if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) else mt() - let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) + let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp) - let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) + let pr_sep_com sep f c = pr_with_comments ~loc:(constr_loc c) (sep() ++ f c) let pr_univ l = match l with @@ -302,7 +302,7 @@ let tag_var = tag Tag.variable assert false in let loc = cases_pattern_expr_loc (loc, p) in - pr_with_comments loc + pr_with_comments ~loc (sep() ++ if prec_less prec inh then strm else surround strm) let pr_patt = pr_patt mt @@ -310,7 +310,7 @@ let tag_var = tag Tag.variable let pr_eqn pr (loc,(pl,rhs)) = let pl = List.map snd pl in spc() ++ hov 4 - (pr_with_comments loc + (pr_with_comments ~loc (str "| " ++ hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ @@ -730,7 +730,7 @@ let tag_var = tag Tag.variable return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) in let loc = constr_loc a in - pr_with_comments loc + pr_with_comments ~loc (sep() ++ if prec_less prec inherited then strm else surround strm) type term_pr = { diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index f92caf426..482c994c2 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -35,7 +35,7 @@ val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_lident : Id.t located -> std_ppcmds val pr_lname : Name.t located -> std_ppcmds -val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds +val pr_with_comments : ?loc:Loc.t -> std_ppcmds -> std_ppcmds val pr_com_at : int -> std_ppcmds val pr_sep_com : (unit -> std_ppcmds) -> diff --git a/printing/pputils.ml b/printing/pputils.ml index e90b54685..4ae5035a2 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -15,7 +15,7 @@ open Locus open Genredexpr let pr_located pr (loc, x) = - if !Flags.beautify && loc <> Loc.ghost then + if !Flags.beautify && not (Loc.is_ghost loc) then let (b, e) = Loc.unloc loc in (* Side-effect: order matters *) let before = Pp.comment (CLexer.extract_comments b) in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 96b0f49d4..025514902 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -539,7 +539,7 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in + let c = Notation_ops.glob_constr_of_notation_constr a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ @@ -752,7 +752,7 @@ let print_any_name = function let print_name = function | ByNotation (loc,(ntn,sc)) -> print_any_name - (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference ~loc (fun _ -> true) ntn sc)) | AN ref -> print_any_name (locate_any_name ref) @@ -800,7 +800,7 @@ let print_about_any loc k = let print_about = function | ByNotation (loc,(ntn,sc)) -> print_about_any loc - (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference ~loc (fun _ -> true) ntn sc)) | AN ref -> print_about_any (loc_of_reference ref) (locate_any_name ref) diff --git a/printing/printer.ml b/printing/printer.ml index 35ddf2e8c..279295a03 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -196,10 +196,10 @@ let qualid_of_global env r = let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in - let extern_ref loc vars r = - try orig_extern_ref loc vars r + let extern_ref ?loc vars r = + try orig_extern_ref ?loc vars r with e when CErrors.noncritical e -> - Libnames.Qualid (loc, qualid_of_global env r) + Libnames.Qualid (Loc.tag ?loc @@ qualid_of_global env r) in Constrextern.set_extern_reference extern_ref; try |