From fca82378cd2824534383f1f5bc09d08fade1dc17 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Apr 2018 18:21:49 +0200 Subject: [api] Move bullets and goals selectors to `proofs/` `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select` --- parsing/g_vernac.ml4 | 1 + 1 file changed, 1 insertion(+) (limited to 'parsing') diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2dbd624c2..3026be248 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 -- cgit v1.2.3