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

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 1e759930ac4ef706175c85c181244657e3dd5558..c82919f4d693640891588165a30ee9e1662c1ad7 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -144,7 +144,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
     | Ast.Implicit `Vector -> "?"
-    | Ast.Implicit `JustOne -> "..."
+    | Ast.Implicit `JustOne -> "…"
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 1dab53582f590d6addf47af680be5cfe25580799..21031d002fc10fba43eb915623f054d45743ecd0 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -69,7 +69,6 @@ let regexp delim_end = "\\]"
 let regexp qkeyword = "'" ( ident | pident ) "'"
 
 let regexp implicit = '?'
-let regexp implicit_vector = "..."
 let regexp placeholder = '%'
 let regexp meta = implicit number
 
@@ -317,7 +316,6 @@ and level2_ast_token =
      let s = Ulexing.utf8_lexeme lexbuf in
       return lexbuf ("META", String.sub s 1 (String.length s - 1))
   | implicit -> return lexbuf ("IMPLICIT", "")
-  | implicit_vector -> return lexbuf ("IMPLICITVECTOR", "")
   | placeholder -> return lexbuf ("PLACEHOLDER", "")
   | ident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 2ac6b7e6a4ad31e702b9c58768c09f7effcd50d2..af9edd9be226bb54bd30f714df9144b70ebd6c1c 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -757,7 +757,7 @@ EXTEND
       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
       | n = NUMBER -> return_term loc (Ast.Num (n, 0))
       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
-      | IMPLICITVECTOR -> return_term loc (Ast.Implicit `Vector)
+      | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
       | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
       | m = META; s = meta_substs ->

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 5e8f26a4f7758deb8816c37633b97e0b2b2d15b7..c115fe018efb8d4698f8bea0c36cacf059f9521f 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -254,7 +254,7 @@ let pp_ast0 t k =
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
     | Ast.Implicit `JustOne -> builtin_symbol "?"
-    | Ast.Implicit `Vector -> builtin_symbol "..."
+    | Ast.Implicit `Vector -> builtin_symbol "…"
     | Ast.Meta (n, l) ->
         let local_context l =
             List.map (function None -> None | Some t -> Some (k t)) l

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 =