diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-15 14:48:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-17 18:16:11 +0200 |
| commit | a8088f565da008d3b1780f38de0ee894e8fd0baa (patch) | |
| tree | f03b8d5eb42e69dab608cc6a30a2953283f86fbd | |
| parent | 42cbdfccf0c0500935d619dccaa00476690229f8 (diff) | |
Set required version of camlp5 to 6.06.
It is already very old (shipped with Debian oldstable) and adds file name
support in locations.
| -rw-r--r-- | configure.ml | 4 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 17 |
2 files changed, 3 insertions, 18 deletions
diff --git a/configure.ml b/configure.ml index 71502058f..ae71066a8 100644 --- a/configure.ml +++ b/configure.ml @@ -537,9 +537,9 @@ let check_camlp5_version camlp5o = let version_line, _ = run ~err:StdOut camlp5o ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in match string_split '.' version with - | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) -> + | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> printf "You have Camlp5 %s. Good!\n" version; version - | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n" + | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" let check_caml_version_for_camlp4 () = if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 2b67693d2..e79001ee3 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -20,14 +20,8 @@ end exception Exc_located = Ploc.Exc -IFDEF CAMLP5_6_00 THEN -let ploc_file_name = Ploc.file_name -ELSE -let ploc_file_name _ = "" -END - let to_coqloc loc = - Loc.create (ploc_file_name loc) (Ploc.line_nb loc) + Loc.create (Ploc.file_name loc) (Ploc.line_nb loc) (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc) let make_loc = Ploc.make_unlined @@ -131,11 +125,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in Loc.raise loc e -IFDEF CAMLP5_6_02_1 THEN let entry_print ft x = Entry.print ft x -ELSE - let entry_print _ x = Entry.print x -END let srules' = Gramext.srules let parse_tokens_after_filter = Entry.parse_token end @@ -216,13 +206,8 @@ ELSE | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok) END -IFDEF CAMLP5_6_00 THEN let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) -ELSE - let slist0sep (x, y) = Gramext.Slist0sep (x, y) - let slist1sep (x, y) = Gramext.Slist1sep (x, y) -END let snterml (x, y) = Gramext.Snterml (x, y) let snterm x = Gramext.Snterm x |