Fixing indexing (commit parziale di Claudio?)

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 1058a48cca4a0faaa09ee2609d4f10a9dc522b08..1a793b92fde5db51b370c46eac38a5343f188058 100644 (file)
--- 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;;