*** empty log message ***

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 197ceffbbbb6e06e48bd13cec42bba11eba34f34..e8afa80329fd9572a2a70ef8e25d0bc3d3396563 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -1238,7 +1238,7 @@ let main dbd term metasenv ugraph =
 ;;
 
 
-let saturate dbd (proof, goal) =
+let saturate dbd ?(full=false) ?(depth=0) ?(width=0) (proof, goal) =
   let module C = Cic in
   maxmeta := 0;
   let goal' = goal in