From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 tools/coqdoc/index.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'tools/coqdoc/index.ml')

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index a28e1197..a2cb995e 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,13 +1,13 @@
 (* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.ml 13676 2010-12-04 10:34:21Z herbelin $ i*)
+(*i $Id: index.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Filename
 open Lexing
@@ -61,8 +61,10 @@ let full_ident sp id =
   then id
   else ""
 
-let add_def loc ty sp id =
-  Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
+let add_def loc1 loc2 ty sp id =
+  for loc = loc1 to loc2 do
+    Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+  done;
   Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
 
 let add_ref m loc m' sp id ty =
@@ -341,16 +343,16 @@ let read_glob f =
 		    for loc=loc1 to loc2 do
 		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
 		    done)
-	       with _ ->
-	       try
-		Scanf.sscanf s "R%d %s %s %s %s"
-		  (fun loc lib_dp sp id ty ->
-		    add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
 	       with _ -> ())
 	  | _ ->
-	      try Scanf.sscanf s "%s %d %s %s"
-		(fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
+	      try Scanf.sscanf s "not %d %s %s"
+		(fun loc sp id -> add_def loc loc (type_of_string "not") sp id)
+	      with Scanf.Scan_failure _ ->
+	      try Scanf.sscanf s "%s %d:%d %s %s"
+		(fun ty loc1 loc2 sp id ->
+                  add_def loc1 loc2 (type_of_string ty) sp id)
 	      with Scanf.Scan_failure _ -> ()
+
       end
     done; assert false
   with End_of_file ->
-- 
cgit v1.2.3