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 e8a95fc892f7984afb25ede9f630279afe3fb859..49468eafbefad7e1ae9484f5f0e502f6fd308ee7 100644 (file)
--- 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 74d5301820f7e1ec6c8700515ac7168f71304b2a..a1c19fa578bcfb6c60ae19df4b6dcd0a07be43f5 100644 (file)
--- 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