diff options
| author |  Carst Tankink <carst.tankink@inria.fr> | 2014-04-10 11:03:12 +0200 |
|---|---|---|
| committer |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-10 19:43:08 +0200 |
| commit | 546d47608f944d9463aaf49ec00dee026fe32818 (patch) | |
| tree | 3fe6266bb3fbbaa2295ec723901e2290e62c48fd /tools/coqdoc/index.ml | |
| parent | 7477094b353b48f1bd1f8ee97a8cd69c04be9db9 (diff) | |
Dumpglob: factor out reference dumping.
Factored out all functions that dump references to use one function
"dump_ref"
Diffstat (limited to 'tools/coqdoc/index.ml')
| -rw-r--r-- | tools/coqdoc/index.ml | 3 |
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) |