ppterm added

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        *)

diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli
index 99757d1862882d9eaa1542217539a29d77687ed6..8d9071fcc4aa77cae6c780d3a41eabc7bdeb4497 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.mli
+++ b/helm/ocaml/cic_proof_checking/cicPp.mli
@@ -39,3 +39,5 @@
 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
 (* similar to the one used by Coq                                             *)
 val ppobj : Cic.obj -> string
+
+val ppterm : Cic.term -> string