Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constants

Reviewed-by: ppedrot

1 files changed, 5 insertions, 5 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4afed07eda..fdf0db9909 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1009,11 +1009,11 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
     let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in
     let app' = f acc app in
     let a' = f acc a in
-      (match EConstr.kind sigma app' with
-      | App (hdf', al') when hdf' == hdf ->
-        (* Still the same projection, we ignore the change in parameters *)
-        mkProj (p, a')
-      | _ -> mkApp (app', [| a' |]))
+    let hdf', _ = decompose_app_vect sigma app' in
+    if hdf' == hdf then
+      (* Still the same projection, we ignore the change in parameters *)
+      mkProj (p, a')
+    else mkApp (app', [| a' |])
   | _ -> map_constr_with_binders_left_to_right sigma g f acc c
 
 let e_contextually byhead (occs,c) f = begin fun env sigma t ->