From 246f3c2f2d26655129efacf830ecff47094795b4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Apr 2009 15:24:45 +0000 Subject: [PATCH] removed spurious " --- helm/software/components/ng_kernel/nCicPp.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index c4c66374a..5b4c9940c 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -186,7 +186,7 @@ let rec ppcontext ?(sep="\n") ~subst ~metasenv = function let rec ppmetasenv ~subst metasenv = function | [] -> "" | (i,(name, ctx, ty)) :: tl -> - let name = match name with Some n -> "(\""^n^"\")" | _ -> "" in + let name = match name with Some n -> "("^n^")" | _ -> "" in ppcontext ~sep:"; " ~subst ~metasenv ctx ^ " ⊢ ?"^string_of_int i^name^" : " ^ ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^ @@ -212,6 +212,7 @@ let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;; let ppobj (u,_,metasenv, subst, o) = "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^ + "subst:\n" ^ ppsubst subst ~metasenv ^ "\n" ^ match o with | NCic.Fixpoint (b, fl, _) -> "{"^NUri.string_of_uri u^"}\n"^ -- 2.39.2