cbn leaves behind unnamable constants when asked to reduce Pos.add_carry

[JasonGross]

Description of the problem

From Coq Require Import PArith.
Local Open Scope positive_scope.
Goal Pos.add 1021 53 = Pos.add 1021 53.
  assert_succeeds (cbv [Pos.add Pos.add_carry Pos.succ]; assert_fails progress cbv).
  assert_succeeds (cbn; assert_fails progress cbv).
  cbn [Pos.add Pos.add_carry Pos.succ]; assert_succeeds progress cbv. (* huh? *)

  lazymatch goal with
  | [ |- (?f 510 26)~0 = (?f 510 26)~0 ]
    => unify f Pos.add_carry;
       idtac f (* Pos.add_carry *)
  end.
  Fail lazymatch goal with
  | [ |- (?f 510 26)~0 = (?f 510 26)~0 ]
    => constr_eq f Pos.add_carry
       end.
  (* The command has indeed failed with message:
Tactic failure: Not equal.
   *)
  Fail progress cbv [Pos.add_carry].
  (* The command has indeed failed with message:
Failed to progress.
   *)
  Set Debug "Cbv".
  cbv [Coq.PArith.BinPos.Pos.add_carry].
  (* Huh? Debug: [Cbv] Not unfolding Coq.PArith.BinPos.Pos.add_carry
Debug: [Cbv] Not unfolding Coq.PArith.BinPos.Pos.add_carry
*)
  cbv. (* Debug: [Cbv] Unfolding Coq.PArith.BinPos.Pos.add_carry
Debug: [Cbv] Unfolding Coq.PArith.BinPos.Pos.succ
*)

Presumably this is something to do with mismatched kernel/canonical names?

Coq Version

8.17

[herbelin]

Indeed a canonical/user name problem! Fixed in #18616.