diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b3bc895ba..a1c563f53 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -48,6 +48,7 @@ let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" let make_bullet s = + let open Proof_bullet in let n = String.length s in match s.[0] with | '-' -> Dash n |