diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5f358e6944..936d960d79 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -138,7 +138,7 @@ let coqdoc_unfreeze (lt,tn,lp) = token_number := tn; last_pos := lp -let add_glob loc ref = +let split_global ref = let sp = Nametab.sp_of_global ref in let lib_dp = Lib.library_part ref in let mod_dp,id = repr_path sp in @@ -147,6 +147,12 @@ let add_glob loc ref = let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath fullname) +let add_glob loc ref = + let file,fields,id = split_global ref in + let filepath = string_of_dirpath file in + let modpath = string_of_qualid (make_qualid fields id) in + dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath modpath) + let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) else snd (unloc (f (List.hd args))) |