From 8304a104ea201db83bbe82430cbb29dd495dab10 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 3 Feb 2006 15:08:24 +0000 Subject: [PATCH] Modified lambda and explicit substitutions. --- helm/ocaml/cic_proof_checking/cicPp.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 53f52272a..954134584 100644 --- 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 = -- 2.39.2