removed spurious "

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index c4c66374a622b59965efdf611d262aa495732bde..5b4c9940cbd623c700c197b501d937a5a04ab5f3 100644 (file)
--- 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"^