From de988641848ecb26f749fbc3f50ce9194db46a4c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 24 Jan 2018 16:45:46 +0100 Subject: Use r.(p) syntax to print primitive projections. There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems. --- printing/ppconstr.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 51735bc9e..1146b42a0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -732,6 +732,9 @@ let tag_var = tag Tag.variable return (pr_prim_token p, prec_of_prim_token p) | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) + | CProj (p,c) -> + let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in + return (p, lproj) in let loc = constr_loc a in pr_with_comments ?loc -- cgit v1.2.3