diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-14 00:26:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-14 10:28:27 +0200 |
| commit | 684dd06c538ea6024e5dd01bfc6eb416b08ddc14 (patch) | |
| tree | 4f5b011b96b0afea2a5d2b1877df8be64f7e898d /toplevel | |
| parent | 3b6d89acf4f233d0ed33f89c4e60bcd68e0e2820 (diff) | |
Removing a variable warned unused.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |