From 15eb6b5721aaff1281f1f71e00c98fd9a39511e0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 6 Mar 2020 21:20:17 +0100
Subject: Fix #9930: "change" replaces 0-param projections by constants

---
 pretyping/tacred.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

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 ->
-- 
cgit v1.2.3