X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=1a793b92fde5db51b370c46eac38a5343f188058;hb=dd29593d12cffd332c9d546167215f42a90fa9f7;hp=1058a48cca4a0faaa09ee2609d4f10a9dc522b08;hpb=d02e9de60490bc1928ca7d32db2263e21c0148de;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 1058a48cc..1a793b92f 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -224,7 +224,9 @@ let ppmetaattrs =
     String.concat ","
      (List.map
        (function
-           `IsSort -> "sort"
+         | `IsTerm -> "term"
+         | `IsType -> "type"
+         | `IsSort -> "sort"
          | `Name n -> "name=" ^ n
          | `InScope -> "in_scope"
          | `OutScope n -> "out_scope:" ^ string_of_int n
@@ -259,8 +261,9 @@ let rec ppsubst ~formatter ~subst ~metasenv = function
       ppsubst ~formatter ~subst ~metasenv tl
 ;;
 
-let ppsubst ~formatter ~metasenv subst =
- ppsubst ~formatter ~metasenv ~subst subst
+let ppsubst ~formatter ~metasenv ?(use_subst=true) subst =
+ let ssubst = if use_subst then subst else [] in
+  ppsubst ~formatter ~metasenv ~subst:ssubst subst
 ;;
 
 let string_of_generated = function
@@ -353,7 +356,9 @@ let ppcontext ?sep ~subst ~metasenv ctx =
 
 let ppmetasenv ~subst metasenv = on_buffer (ppmetasenv ~subst) metasenv;;
 
-let ppsubst ~metasenv subst = on_buffer (ppsubst ~metasenv) subst;;
+let ppsubst ~metasenv ?use_subst subst =
+ on_buffer (ppsubst ~metasenv ?use_subst) subst
+;;
 
 let ppobj obj = on_buffer ppobj obj;;