"..." -> "\ldots" for implicit vectors

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index a7b6559a6520300c108b3167272264bce37f70cc..7d7a90dcc9e5933d94650011e5db3dd6b3498031 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -60,7 +60,7 @@ let string_of_implicit_annotation = function
   | `Hole -> "□"
   | `Term -> "Term"
   | `Typeof x -> "Ty("^string_of_int x^")"
-  | `Vector -> "..."
+  | `Vector -> "…"
 ;;
 
 let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t =