From c0f26dd0ebae4bad9a8850a198f0126ea4656e73 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2006 18:17:38 +0000
Subject: Changement de précédence de l'argument du by de assert;
 conséquences sur les .v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'interp')

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)))
-- 
cgit v1.2.3