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

Reviewed-by: ppedrot

3 files changed, 24 insertions, 7 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 ->
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index 25285622a9..bad9d64f65 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -4,9 +4,10 @@ Set Primitive Projections.
 Record params := { width : Z }.
 Definition p : params := Build_params 64.
 
+Definition width' := width.
 Set Printing All.
 
-Goal width p = 0%Z -> width p = 0%Z.
+Lemma foo : width p = 0%Z -> width p = 0%Z.
   intros.
 
   assert_succeeds (enough True; [omega|]).
@@ -16,7 +17,9 @@ Goal width p = 0%Z -> width p = 0%Z.
 (*   ============================ *)
 (*   @eq Z (width p) Z0 *)
 
-  change tt with tt in H.
+  change (width' p = 0%Z) in H;cbv [width'] in H.
+  (* check that we correctly got the compat constant in H *)
+  Fail match goal with H : ?l = _ |- ?l' = _ => constr_eq l l' end.
 
 (*   H : @eq Z (width p) Z0 *)
 (*   ============================ *)
diff --git a/test-suite/bugs/closed/bug_9930.v b/test-suite/bugs/closed/bug_9930.v
new file mode 100644
index 0000000000..042cd69fbe
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9930.v
@@ -0,0 +1,14 @@
+Set Primitive Projections.
+Record params := { width : nat }.
+Definition p : params := Build_params 64.
+
+Lemma foo : width p = 0 -> width p = 0.
+  intros.
+  let e := lazymatch type of H with ?e = 0 => e end in
+  change tt with tt in H;
+  let E := lazymatch type of H with ?E = 0 => E end in
+  idtac "before:" e; idtac "after :" E;
+  (* before: (width p) *)
+  (* after : (width p) *)
+  tryif constr_eq e E then exact H else idtac.
+Qed.