BIG FAT COMMIT REGARDING COERCIONS:

[helm.git] / helm / software / components / cic_proof_checking / cicPp.ml

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index e44c6b5881be2f47d260c66c6ed91142416ffd7a..06bb082b4110b531209d55321e4aa9e4f4763b15 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -95,14 +95,14 @@ let rec pp t l =
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
-        | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+          C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+        | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
     | C.LetIn (b,s,t) ->
-       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right