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.

1 files changed, 6 insertions, 0 deletions

diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index be8abb92e..b4ca1073c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,6 +109,7 @@ let change_vars =
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
+      | GProj(p,c) -> GProj(p, change_vars mapping c)
       ) rt
   and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
     let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -293,6 +294,7 @@ let rec alpha_rt excluded rt =
 	GApp(alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
 	    )
+    | GProj(p,c) -> GProj(p, alpha_rt excluded c)
   in
   new_rt
 
@@ -344,6 +346,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
+    | GProj (_,c) -> is_free_in c
     ) x
   and is_free_in_br (_,(ids,_,rt)) =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -437,6 +440,8 @@ let replace_var_by_term x_id term =
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
 		Miscops.map_cast_type replace_var_by_pattern c)
+      | GProj(p,c) ->
+        GProj(p,replace_var_by_pattern c)
     ) x
   and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
     if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -540,6 +545,7 @@ let expand_as =
       | GCases(sty,po,el,brl) ->
 	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
+      | GProj(p,c) -> GProj(p, expand_as map c)
     )
   and expand_as_br map (loc,(idl,cpl,rt)) =
     (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))