diff options
| author | herbelin | 2004-07-16 21:16:56 +0000 |
|---|---|---|
| committer | herbelin | 2004-07-16 21:16:56 +0000 |
| commit | 4cfc8344bae87d5749ce6b553e2d5e2f98ca883b (patch) | |
| tree | 39e1e9c5a91d1e50c64e186637787020862f25d0 /parsing | |
| parent | 5a947f0317aa627b129332d2f38167ebd1bb9c31 (diff) | |
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 8 |
3 files changed, 7 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0a93473604..b653654589 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -31,6 +31,7 @@ let thm_token = G_proofs.thm_token (* compilation on PowerPC and Sun architectures *) let filter_com (b,e) = + let (b,e) = unloc (b,e) in Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments if !Options.v7 then diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 63aecdcb47..c016d86f7c 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -147,7 +147,7 @@ let init () = let _ = init() (* Errors occuring while lexing (explained as "Lexer error: ...") *) -let err loc str = Stdpp.raise_with_loc loc (Error str) +let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str) (* The string buffering machinery *) @@ -480,7 +480,7 @@ let loct_func loct i = else if !loct.(i/tsz) = [| |] then None else !loct.(i/tsz).(i mod tsz) with - | Some loc -> loc + | Some loc -> Util.make_loc loc | _ -> locerr () let loct_add loct i loc = diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a54754e7d3..f9c8d53295 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,12 +8,11 @@ (* $Id$ *) +open Util open Names open Libnames open Q_util -let dummy_loc = (0,0) - let is_meta s = String.length s > 0 && s.[0] == '$' let purge_str s = @@ -22,7 +21,8 @@ let purge_str s = let anti loc x = let e = - let loc = (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >> + let loc = unloc loc in + let loc = make_loc (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >> in <:expr< $anti:e$ >> @@ -110,7 +110,7 @@ and expr_list_of_var_list sl = (* We don't give location for tactic quotation! *) let loc = dummy_loc -let dloc = <:expr< (0,0) >> +let dloc = <:expr< Util.dummy_loc >> let mlexpr_of_ident id = <:expr< Names.id_of_string $str:Names.string_of_id id$ >> |