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 /vernac | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 12 |
4 files changed, 2 insertions, 16 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index b9c4c6cc5..015552d68 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -28,8 +28,6 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration -let out_punivs = Univ.out_punivs - (**********************************************************************) (* Generic synthesis of boolean equality *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f86a0ef92..bb5be4cb0 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -527,7 +527,7 @@ let warn_skip_spaces_curly = (fun () ->strbrk "Skipping spaces inside curly brackets") let rec drop_spacing = function - | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt + | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt | fmt -> fmt diff --git a/vernac/record.ml b/vernac/record.ml index 8b4b7606f..53722b8f6 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -216,7 +216,7 @@ let warning_or_error coe indsp err = (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in if coe then user_err ~hdr:"structure" st; - Flags.if_verbose Feedback.msg_info (hov 0 st) + warn_cannot_define_projection (hov 0 st) type field_status = | NoProjection of Name.t diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index a1835959c..e44b585d7 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -106,8 +106,6 @@ module Tag = struct end -type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit - let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () @@ -283,16 +281,6 @@ let print_err_exn ?extra any = let msg = CErrors.iprint (e, info) ++ fnl () in std_logger ~pre_hdr Feedback.Error msg -(* Output to file, used only in extraction so a candidate for removal *) -let ft_logger old_logger ft ?loc level mesg = - let id x = x in - match level with - | Debug -> msgnl_with ft (make_body id dbg_hdr mesg) - | Info -> msgnl_with ft (make_body id info_hdr mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ?loc level mesg - | Error -> old_logger ?loc level mesg - let with_output_to_file fname func input = (* XXX FIXME: redirect std_ft *) (* let old_logger = !logger in *) |