]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralOptimizer.mli
a few missing ~subst added to whd
[helm.git] / helm / software / components / acic_procedural / proceduralOptimizer.mli
index 45505d72cc098f1c96c047c97657a5e4520c193b..1e7bdada259d1100ee5146beaa34402812f0641a 100644 (file)
@@ -23,4 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val optimize_obj: Cic.obj -> Cic.obj
+val optimize_obj: Cic.obj -> Cic.obj * string
+
+val optimize_term: Cic.context -> Cic.term -> Cic.term * string
+
+val debug: bool ref