X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=c2ee6a776cba5d8d223b99ec9bf3eecf7d77d1e9;hb=0920a5755553774f5b41d7603318ea997ecbdca5;hp=0d868c0027e1f0e7a53a8755086f213f5ba747ed;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 0d868c002..c2ee6a776 100644
--- 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" 
@@ -140,10 +140,13 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
     | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
     | Ast.NRef nref -> NReference.string_of_reference nref
+    | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic
     | 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.Implicit (`Tagged name) -> "?"^name
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
@@ -166,7 +169,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
@@ -294,10 +297,12 @@ let pp_fields pp_term fields =
     (List.map 
       (fun (name,ty,coercion,arity) -> 
         " " ^ name ^ 
-        if coercion then (":" ^ 
-          if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
-        pp_term ty) fields)
-        
+        (if coercion then 
+	  (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ") 
+	else ": ") ^
+      pp_term ty)
+    fields)
+
 let pp_obj pp_term = function
  | Ast.Inductive (params, types) ->
     let pp_constructors constructors =
@@ -318,9 +323,9 @@ let pp_obj pp_term = function
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+ | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
     sprintf "<<pretty printing of mutual definitions not implemented yet>>"
- | Ast.Theorem (flavour, name, typ, body) ->
+ | Ast.Theorem (flavour, name, typ, body,_) ->
     sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)
       name