From 684dd06c538ea6024e5dd01bfc6eb416b08ddc14 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 14 May 2017 00:26:16 +0200 Subject: Removing a variable warned unused. --- toplevel/metasyntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 349c05a38..0787b058a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -520,7 +520,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 -- cgit v1.2.3