diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /parsing | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml4 | 8 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 4 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 7 |
4 files changed, 0 insertions, 24 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index f25b394f0..18942ac29 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -114,9 +114,6 @@ module Error = struct | UnsupportedUnicode x -> Printf.sprintf "Unsupported Unicode character (0x%x)" x) - (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) - end open Error @@ -153,10 +150,6 @@ let bump_loc_line_last loc bol_pos = in Ploc.encl loc loc' -let set_loc_file loc fname = - Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc) - (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) - (* For some reason, the [Ploc.after] function of Camlp5 does not update line numbers, so we define our own function that does it. *) let after loc = @@ -434,7 +427,6 @@ let push_char c = real_push_char c let push_string s = Buffer.add_string current_comment s -let push_bytes s = Buffer.add_bytes current_comment s let null_comment s = let rec null i = diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 496b20002..65e99d1b9 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -80,10 +80,6 @@ let create_pos = function | None -> Extend.First | Some lev -> Extend.After (constr_level lev) -type gram_level = - gram_position option * gram_assoc option * string option * - (** for reinitialization: *) gram_reinit option - let find_position_gen current ensure assoc lev = match lev with | None -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 011565d86..3438635cf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -756,11 +756,6 @@ GEXTEND Gram implicit_status = MaximallyImplicit}) items ] ]; - name_or_bang: [ - [ b = OPT "!"; id = name -> - not (Option.is_empty b), id - ] - ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ [ name = name -> [(snd name, Vernacexpr.NotImplicit)] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index dad98e2e9..3f014c4c8 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -171,7 +171,6 @@ module Symbols : sig val sopt : G.symbol -> G.symbol val snterml : G.internal_entry * string -> G.symbol val snterm : G.internal_entry -> G.symbol - val snterml_level : G.symbol -> string end = struct let stoken tok = @@ -199,10 +198,6 @@ end = struct let slist1 x = Gramext.Slist1 x let sopt x = Gramext.Sopt x - let snterml_level = function - | Gramext.Snterml (_, l) -> l - | _ -> failwith "snterml_level" - end let camlp4_verbosity silent f x = @@ -211,8 +206,6 @@ let camlp4_verbosity silent f x = f x; warning_verbose := a -let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x - (** Grammar extensions *) (** NB: [extend_statment = |