Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope)#23

Merged

pi8027 merged 1 commit intomasterfrom function_scope

Dec 8, 2023

+2-2

Commits on Dec 7, 2023

Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope)
pi8027
committed