From 546d47608f944d9463aaf49ec00dee026fe32818 Mon Sep 17 00:00:00 2001
From: Carst Tankink
Date: Thu, 10 Apr 2014 11:03:12 +0200
Subject: Dumpglob: factor out reference dumping.

Factored out all functions that dump references to use one function
"dump_ref"
---
 tools/coqdoc/index.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8e82f45771..980f805efe 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -339,9 +339,6 @@ let read_glob vfile f =
 		    done)
 	       with _ -> ())
 	  | _ ->
-	      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)
-- 
cgit v1.2.3