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.

3 files changed, 11 insertions, 1 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0b929b8ca..f7639d22d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
+            | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
 	end (* end of the application treatement *)
 
@@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GCast(b,_) ->
 	build_entry_lc env funnames  avoid b
+    | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
     (brl:Glob_term.cases_clauses) avoid :
@@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
 		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ ->
+  | GIf _ | GRec _ | GCast _ | GProj _ ->
       raise (UserError(Some "compute_cst_params", str "Not handled case"))
   ) gt
 and compute_cst_params_from_app acc (params,rtl) =
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))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 071bab2f3..58154d310 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -215,6 +215,7 @@ let is_rec names =
     | GCases(_,_,el,brl) ->
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
+    | GProj(_,c) -> lookup names c
   and lookup_br names (_,(idl,_,rt)) =
     let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
@@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
   | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
   | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+  | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
   )
 exception Stop of  Constrexpr.constr_expr