From 67ff18bfa019d95daa1ce9f132943b70b791ed02 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Dec 2001 09:18:54 +0000 Subject: [PATCH] ppterm added --- helm/ocaml/cic_proof_checking/cicPp.ml | 4 ++++ helm/ocaml/cic_proof_checking/cicPp.mli | 2 ++ 2 files changed, 6 insertions(+) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 97ae6a50f..745a203a4 100644 --- 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 99757d186..8d9071fcc 100644 --- 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 -- 2.39.2