diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-14 17:09:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-14 17:09:03 +0000 |
| commit | 36288ae15ec523b78603084777216a7d90057ba1 (patch) | |
| tree | cfb689aaf831824410f5760266b397170280ebe3 | |
| parent | c537cc15c60cf974d87749ca17b02b3ebafec4f9 (diff) | |
Dumpglob.dump_modref : fix an assert failure
The list obtained as second part of a Lib.split_modpath *can* be
empty, for instance when mp is a MPfile, so calling on it
Util.list_drop_last may fail.
Can somebody knowledgeable in the dump mechanism (Jean-Marc ?)
check that my simplistic fix is correct ?
For information, I've ended on this failure while playing with
a rather unnatural example: take a .v file, consider it as a
module and apply it to a functor...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11450 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/dumpglob.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 0035b3f07..f9881673d 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -194,8 +194,9 @@ let dump_local_binder b sec ty = let dump_modref loc mp ty = if dump () then let (dp, l) = Lib.split_modpath mp in + let l = if l = [] then l else Util.list_drop_last l in let fp = Names.string_of_dirpath dp in - let mp = Names.string_of_dirpath (Names.make_dirpath (Util.list_drop_last l)) in + let mp = Names.string_of_dirpath (Names.make_dirpath l) in dump_string (Printf.sprintf "R%d %s %s %s %s\n" (fst (Util.unloc loc)) fp mp "<>" ty) |