support axioms

[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 fd9932d9fda963233e11f7a78bfdbf48187dec13..1a793b92fde5db51b370c46eac38a5343f188058 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -195,7 +195,7 @@ let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
   ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t
 ;;
 
-let rec ppcontext ~formatter ?(sep=";") ~subst ~metasenv = function
+let rec ppcontext ~formatter ?(sep="; ") ~subst ~metasenv = function
   | [] -> ()
   | (name, NCic.Decl t) :: tl -> 
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
@@ -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;;