Introduction of vectors of implicit (only for NG).

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 5eb6b64d2ad26fd1c27a3904bb94126a12176b22..1e759930ac4ef706175c85c181244657e3dd5558 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -117,14 +117,14 @@ let rec pp_term ?(pp_parens = true) t =
           (pp_term ~pp_parens:true t3)
     | Ast.LetRec (kind, definitions, term) ->
        let rec get_guard i = function
-          | []                   -> (*assert false*) Ast.Implicit
+          | []                   -> (*assert false*) Ast.Implicit `JustOne
           | [term, _] when i = 1 -> term
           | _ :: tl              -> get_guard (pred i) tl
        in
        let map (params, (id,typ), body, i) =
          let typ =
           match typ with
-             None -> Ast.Implicit
+             None -> Ast.Implicit `JustOne
            | Some typ -> typ
          in
           sprintf "%s %s on %s: %s \\def %s" 
@@ -143,7 +143,8 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Ident (name, Some substs)
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
-    | Ast.Implicit -> "?"
+    | Ast.Implicit `Vector -> "?"
+    | Ast.Implicit `JustOne -> "..."
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
@@ -166,7 +167,7 @@ let rec pp_term ?(pp_parens = true) t =
   in
   match pp_parens, t with
     | false, _ 
-    | true, Ast.Implicit
+    | true, Ast.Implicit _
     | true, Ast.Sort _
     | true, Ast.Ident (_, Some []) 
     | true, Ast.Ident (_, None)    -> t_pp