diff options
author | 2004-07-16 21:16:56 +0000 | |
---|---|---|
committer | 2004-07-16 21:16:56 +0000 | |
commit | 4cfc8344bae87d5749ce6b553e2d5e2f98ca883b (patch) | |
tree | 39e1e9c5a91d1e50c64e186637787020862f25d0 /interp | |
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 'interp')
-rw-r--r-- | interp/constrextern.mli | 1 | ||||
-rw-r--r-- | interp/constrintern.ml | 10 |
2 files changed, 7 insertions, 4 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 596413660..4bc0c6fa2 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -9,6 +9,7 @@ (*i $Id$ *) (*i*) +open Util open Names open Term open Termops diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6c0febecf..9217400bc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -155,10 +155,11 @@ let add_glob loc ref = let sp = Nametab.sp_of_global ref in let id = let _,id = repr_path sp in string_of_id id in let dp = string_of_dirpath (Lib.library_part ref) in - dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id) + dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id) let loc_of_notation f loc args ntn = - if args=[] or ntn.[0] <> '_' then fst loc else snd (f (List.hd args)) + if args=[] or ntn.[0] <> '_' then fst (unloc loc) + else snd (unloc (f (List.hd args))) let ntn_loc = loc_of_notation constr_loc let patntn_loc = loc_of_notation cases_pattern_loc @@ -166,7 +167,8 @@ let patntn_loc = loc_of_notation cases_pattern_loc let dump_notation_location = fun pos ntn ((path,df),sc) -> let rec next growing = - let (bp,_ as loc) = Lexer.location_function !token_number in + let loc = Lexer.location_function !token_number in + let (bp,_) = unloc loc in if growing then if bp >= pos then loc else (incr token_number;next true) else if bp = pos then loc else if bp > pos then (decr token_number;next false) @@ -175,7 +177,7 @@ let dump_notation_location = last_pos := pos; let path = string_of_dirpath path in let sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst loc) path df sc) + dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) (**********************************************************************) (* Contracting "{ _ }" in notations *) |