From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:54:55 +0200 Subject: [api] Misctypes removal: miscellaneous aliases. --- vernac/metasyntax.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/metasyntax.ml') diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 2245e762f..8f64f5519 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -92,7 +92,7 @@ let pr_grammar = function (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) -let parse_format ({CAst.loc;v=str} : Misctypes.lstring) = +let parse_format ({CAst.loc;v=str} : lstring) = let len = String.length str in (* TODO: update the line of the location when the string contains newlines *) let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in @@ -792,7 +792,7 @@ type notation_modifier = { only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : Misctypes.lstring option; + format : lstring option; extra : (string * string) list; } @@ -1104,7 +1104,7 @@ module SynData = struct only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : Misctypes.lstring option; + format : lstring option; extra : (string * string) list; (* XXX: Callback to printing, must remove *) -- cgit v1.2.3