Skip to content

Commit b3a5924

Browse files
committed
Ban old Datatype syntax
1 parent 1ffde91 commit b3a5924

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

developers/readme_gen.sml

+3
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,9 @@ val ILLEGAL_STRINGS =
4646
("type_abbrev(\"", "The Type syntax is to be used instead of type_abbrev."),
4747
("overload_on(\"", "Use Overload ... = ``...`` instead of overload_on."),
4848
("Hol_datatype"^"`", "Use Datatype: ... End syntax instead of Hol_datatype."),
49+
("Datatype"^"`", "Use Datatype: ... End syntax instead of Datatype with `"),
50+
(* \226\128\152 corresponds to ‘ *)
51+
("Datatype"^"\226\128\152", "Use Datatype: ... End syntax instead of Datatype\226\128\152."),
4952
("Hol_rel"^"n`","Use Inductive ... End instead of old Hol_reln."),
5053
("Hol_rel"^"n\"","Use Inductive ... End instead of old Hol_reln."),
5154
("Hol_corel"^"n`","Use CoInductive ... End instead of old Hol_coreln.")]

0 commit comments

Comments
 (0)