X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=3fae0f52b05a00ea529b3b3acc96e8b4f46ef2d1;hb=8049c166a37789d7a1b1ca1c3a1174712bbf87ba;hp=85f4a3187ea641290d98c2fd75118e15912fedb0;hpb=3b6baca9f28c7d410e543c19f0d8e8467bf25894;p=helm.git

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 85f4a3187..3fae0f52b 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -94,6 +94,7 @@ let string_of_sort_kind = function
   | `CProp _ -> "CProp"
   | `Type _ -> "Type"
   | `NType s -> "Type[" ^ s ^ "]"
+  | `NCProp s -> "CProp[" ^ s ^ "]"
 
 let map_space f l =
  HExtlib.list_concat
@@ -238,7 +239,7 @@ let pp_ast0 t k =
             (fun (params, name, ty, body, rec_param) ->
               [ break;
                 hvbox false true ([
-                  keyword "and";
+                  keyword "and"; space;
                   name] @
                   params @
                   [space; keyword "on" ; space; rec_param ;space ] @
@@ -252,7 +253,8 @@ let pp_ast0 t k =
           ((hvbox false false
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
-    | Ast.Implicit -> builtin_symbol "?"
+    | Ast.Implicit `JustOne -> 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
@@ -541,6 +543,8 @@ let head_names names env =
             aux ((name, (ty, v)) :: acc) tl
         | Env.TermType _, Env.TermValue _  ->
             aux ((name, (ty, v)) :: acc) tl
+        | Env.OptType _, Env.OptValue _ ->
+            aux ((name, (ty, v)) :: acc) tl
         | _ -> assert false)
     | _ :: tl -> aux acc tl
       (* base pattern may contain only meta names, thus we trash all others *)
@@ -556,6 +560,8 @@ let tail_names names env =
             aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
         | Env.TermType _, Env.TermValue _  ->
             aux ((name, (ty, v)) :: acc) tl
+        | Env.OptType _, Env.OptValue _ ->
+            aux ((name, (ty, v)) :: acc) tl
         | _ -> assert false)
     | binding :: tl -> aux (binding :: acc) tl
     | [] -> acc
@@ -595,7 +601,7 @@ let instantiate_level2 env term =
         Ast.Ident (name, Some (aux_substs env substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _