auto with intro

[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 c82919f4d693640891588165a30ee9e1662c1ad7..c2ee6a776cba5d8d223b99ec9bf3eecf7d77d1e9 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -140,11 +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 `Vector -> "?"
     | Ast.Implicit `JustOne -> "…"
+    | Ast.Implicit (`Tagged name) -> "?"^name
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
@@ -321,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