Merge PR #6651: Use r.(p) syntax to print primitive projections.

1 files changed, 3 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) =