proof2cic now uses Deannotate.deannoate_term instead of having an input

[helm.git] / helm / ocaml / cic_omdoc / content2cic.ml

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;;