Commit 569d10d
committed
submodule: bump my-lang to ca440a0 (Rocq proof-debt closure)
Advances my-lang from bf34f4c to ca440a0. New-on-my-lang:
ca440a0 proofs(coq): land has_type_ind_strong — full Typing.v now builds
0f3210f proofs(coq): fix buildability of Syntax.v + T_BinOp cases
These close the my-lang Typing.v weakening+subsumption+substitution
item from proof-debt-plan.md (the ~130-LOC custom induction scheme
that threads nested Forall IH through T_Array).1 parent 3fef999 commit 569d10d
1 file changed
Lines changed: 1 addition & 1 deletion
Submodule my-lang updated from a464e4a to ca440a0
0 commit comments