From: Claudio Sacerdoti Coen Date: Wed, 31 Mar 2010 13:33:55 +0000 (+0000) Subject: Implicit and UserInput were printed incorrectly. X-Git-Tag: make_still_working~2950 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8e16a71ad825a0ed0a73ff32f14a69bc927c1a9d;p=helm.git Implicit and UserInput were printed incorrectly. From: sacerdot --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index c2ee6a776..f94891375 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -144,8 +144,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 `Vector -> "?" - | Ast.Implicit `JustOne -> "…" + | Ast.Implicit `Vector -> "…" + | Ast.Implicit `JustOne -> "?" | Ast.Implicit (`Tagged name) -> "?"^name | Ast.Meta (index, substs) -> sprintf "%d[%s]" index @@ -160,7 +160,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" | Ast.Symbol (name, _) -> "'" ^ name - | Ast.UserInput -> "" + | Ast.UserInput -> "%" | Ast.Literal l -> pp_literal l | Ast.Layout l -> pp_layout l @@ -170,6 +170,7 @@ let rec pp_term ?(pp_parens = true) t = match pp_parens, t with | false, _ | true, Ast.Implicit _ + | true, Ast.UserInput | true, Ast.Sort _ | true, Ast.Ident (_, Some []) | true, Ast.Ident (_, None) -> t_pp