From 4d7349fb1ecfb173f64fad0a97884d1d8e738904 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 15:58:58 +0000 Subject: [PATCH] proof2cic now uses Deannotate.deannoate_term instead of having an input parameter. --- helm/ocaml/cic_omdoc/content2cic.ml | 6 +----- helm/ocaml/cic_omdoc/content2cic.mli | 4 +--- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index e8a95fc89..49468eafb 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -153,9 +153,5 @@ let proof2cic term2cic p = in proof2cic [] p ;; - - - - - +let proof2cic = proof2cic Deannotate.deannotate_term;; diff --git a/helm/ocaml/cic_omdoc/content2cic.mli b/helm/ocaml/cic_omdoc/content2cic.mli index 74d530182..a1c19fa57 100644 --- a/helm/ocaml/cic_omdoc/content2cic.mli +++ b/helm/ocaml/cic_omdoc/content2cic.mli @@ -32,6 +32,4 @@ (* *) (**************************************************************************) -val proof2cic : - (Cic.annterm -> Cic.term) -> - Cic.annterm Content.proof -> Cic.term +val proof2cic : Cic.annterm Content.proof -> Cic.term -- 2.39.2