From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 20 Jul 2003 15:58:58 +0000 (+0000)
Subject: proof2cic now uses Deannotate.deannoate_term instead of having an input
X-Git-Tag: LucaOK~53
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4d7349fb1ecfb173f64fad0a97884d1d8e738904

proof2cic now uses Deannotate.deannoate_term instead of having an input
parameter.
---

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