etc/symbols
changeset 74291 b83fa8f3a271
parent 74290 b2ad24b5a42c
child 74318 3360ea6b659d
--- a/etc/symbols	Sat Sep 11 13:04:32 2021 +0200
+++ b/etc/symbols	Sat Sep 11 21:16:23 2021 +0200
@@ -489,6 +489,9 @@
 \<^type_syntax>         argument: cartouche
 \<^var>                 argument: cartouche
 \<^oracle_name>         argument: cartouche
+\<^Const>               argument: cartouche
+\<^Const_>              argument: cartouche
+\<^Type>                argument: cartouche
 \<^code>                argument: cartouche
 \<^computation>         argument: cartouche
 \<^computation_conv>    argument: cartouche