Optimize the translation of Elaboration

Author: hewzhew

data/courses.yaml

@@ -698,7 +698,7 @@
     元编程 (metaprogramming) 系统。本课程面向数学家和
     计算机科学家。涵盖的内容包括：类型多态、
     Monads、CIC、子类型化、策略、逻辑、集合、可计算性、终止性、
-    元编程、宏、精化 (Elaboration)、类型合一 (Type Unification) 以及其他证明助手的相关工作。
+    元编程、宏、繁饰 (Elaboration)、类型合一 (Type Unification) 以及其他证明助手的相关工作。
 - name: 密码学导论
   instructor: Matthew Robert Ballard
   institution: 南卡罗来纳大学 (University of South Carolina)

templates/extras/speedup.md

@@ -34,7 +34,7 @@
 
 **权衡：** 证明可能会增加好几行密集的代码，并且现在会按名称提及许多引理，其中任何一个将来都可能被重命名，从而破坏你的证明。
 
-### `精化 (elaboration) 耗时过长`
+### `繁饰 (elaboration) 耗时过长`
 
 在触发该消息的声明中查找 `_`，找出它们被填充的内容，并用相应的显式参数替换它们。