diff options
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 45f8e34b1..a8c108f4e 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -20,7 +20,7 @@ let option_D = ref false let option_w = ref false let option_sort = ref false -let rec warning_mult suf iter = +let warning_mult suf iter = let tab = Hashtbl.create 151 in let check f d = begin try |