*** empty log message ***

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 8ced5388922fe31e384c80a9efa5ec5860a487c9..ed22ef4721745369614be57fc2b65274bea0027f 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -525,8 +525,9 @@ let rec demodulation newmeta env table sign target =
     let time1 = Unix.gettimeofday () in
     
     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
-    let ty, _ =
-      CicTypeChecker.type_of_aux' metasenv context what ugraph
+    let ty =
+      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+      with CicUtil.Meta_not_found _ -> ty
     in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =

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