aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/index.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8e82f4577..980f805ef 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)