Remove useless character_range type (#162)

colis-anr · May 8, 2023 · 87e347c · 87e347c
1 parent 4d03370
commit 87e347c
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/CST.mli b/src/CST.mli
@@ -384,9 +384,6 @@ and character_class =
 and class_name =
   | ClassName of string (* Keyword in the current LC_CTYPE category. *)
 
-and character_range =
-  | Range of char list
-
 and variable =
   | VariableAtom of string * variable_attribute