diff options
| author | notin | 2006-05-24 15:52:15 +0000 |
|---|---|---|
| committer | notin | 2006-05-24 15:52:15 +0000 |
| commit | b61f3a445f309c493ab21cd1b521506b7ba34925 (patch) | |
| tree | 85c8cc129e30730f689b3af8376cadecef77facc /interp | |
| parent | f23e2ee0f4d64959288deea74de52fc1a4c45a22 (diff) | |
Adaptation de Coqdoc au nouveau add_glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8861 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5f358e6944..805ffba429 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -145,7 +145,7 @@ let add_glob loc ref = let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in let filepath = string_of_dirpath lib_dp in 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) + dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname) let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) |