[ltac2-logger] Fix bug (dynamic typing assertion).

[rlepigre-skylabs-ai]

This makes the following example (provided by @Janno) work:

Require Import skylabs.ltac2.logger.logger.
Require Import Ltac2.Printf Ltac2.Init.

Ltac2 Log Flag test.
Set SL Debug "test=1".
Set SL Direct Log.
Ltac2 test1 : message -> unit := fun msg => printf "%m" msg.
Ltac2 test2 : message -> unit := fun msg => log[test] "%m" msg.
Ltac2 msg : unit -> message := fun () => fprintf "%t" 'True.

Succeed Ltac2 Eval test1 (msg ()).
Succeed Ltac2 Eval test2 (msg ()).

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/BRiCk/	rodolphe/fix-logger-bug	742a9b2	main	238d10c	#98

Passive Repos

Repo	Job Branch	Job Commit
./	main	655dc44
fmdeps/auto/	main	fbd79d5
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	996d600
bluerock/bhv/	skylabs-main	8030a8f
fmdeps/brick-libcpp/	main	d30c178
fmdeps/ci/	main	9ecdef9
vendored/elpi/	skylabs-master	aa4475f
fmdeps/fm-ci/	main	262fb04
fmdeps/fm-tools/	main	e17f6db
psi/protos/	main	8fe3e7c
psi/backend/	main	99def76
psi/ide/	main	6b596cf
psi/data/	main	1c11c15
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	6060926
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	7c3aae7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.02%	123290.5	123317.1	+26.6	total
-0.00%	22626.6	22626.6	-0.0	├ translation units
+0.03%	100690.5	100663.9	+26.6	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-18.11%	8.7	7.2	-1.6	fmdeps/auto/rocq-skylabs-auto-core/tests/warnings.v
+0.41%	742.7	745.7	+3.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v
+0.66%	194.5	195.8	+1.3	fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v
+0.82%	141.2	142.4	+1.2	bluerock/bhv/apps/vmm/vml/devices/gic/proof/model/gic_hpp_spec.v
+0.92%	321.2	324.1	+3.0	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v
+2.93%	61.6	63.4	+1.8	fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
+19.34%	9.3	11.1	+1.8	fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v
+0.02%	123290.5	123317.1	+26.6	total
-0.00%	22626.6	22626.6	-0.0	├ translation units
+0.03%	100690.5	100663.9	+26.6	└ proofs and tests