Multivariate/vectors.ml: Use </ instead of <#173

jrh13 merged 1 commit intojrh13:masterjrh13/hol-light:masterfrom

dnezam:patch-1dnezam/hol-light:patch-1Copy head branch name to clipboard