ppterm added

[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 97ae6a50f5b8f189f6bc11fe8f145e1a1f3fbe20..745a203a497e9c63de3241129bef2aa9c7a7ad28 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -150,6 +150,10 @@ let rec pp t l =
          "}\n"
 ;;
 
+let ppterm t =
+ pp t []
+;;
+
 (* ppinductiveType (typename, inductive, arity, cons) names                 *)
 (* pretty-prints a single inductive definition (typename, inductive, arity, *)
 (*  cons) where the cic terms in the inductive definition need to be        *)