From 7e52301b501f7a574fca19776fb7fcbfe873d533 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 30 Mar 2010 21:26:06 +0000 Subject: Small things about coqdoc + fixing lettuple.v test (part of bug #2289) In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/dumpglob.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'interp/dumpglob.ml') diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 519f902ba..702c509dc 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -212,6 +212,5 @@ let dump_notation_location posl df (((path,secpath),_),sc) = let secpath = Names.string_of_dirpath secpath in let df = cook_notation df sc in List.iter (fun (bl,el) -> - for pos=bl to el do - dump_string (Printf.sprintf "R%d %s %s %s not\n" pos path secpath df) - done) posl + dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df)) + posl -- cgit v1.2.3