diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index b196bf913..8164910f2 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -591,3 +591,6 @@ let rec string_of_list sep f = function [] -> "" | x :: [] -> f x | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl + +let string_of_intset d = + string_of_list "," string_of_int (Intset.elements d) |