From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Apr 2009 15:24:45 +0000 (+0000)
Subject: removed spurious "
X-Git-Tag: make_still_working~4131
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=246f3c2f2d26655129efacf830ecff47094795b4;p=helm.git

removed spurious "
---

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"^