Modified lambda and explicit substitutions.

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 53f52272aec4d00afab8f15a762ffeee7d3f099c..954134584b69db831d0d060cc0ed2bd301b4bdb0 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -100,7 +100,7 @@ let rec pp t l =
        )
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
-       "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       "(\\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)
     | C.Appl li ->
@@ -185,12 +185,12 @@ let rec pp t l =
          "}\n"
 and pp_exp_named_subst exp_named_subst l =
  if exp_named_subst = [] then "" else
-  "{" ^
+  "\\subst[" ^
    String.concat " ; " (
     List.map
-     (function (uri,t) -> UriManager.name_of_uri uri ^ ":=" ^ pp t l)
+     (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
      exp_named_subst
-   ) ^ "}"
+   ) ^ "]"
 ;;
 
 let ppterm t =