From: Alberto Griggio <griggio@fbk.eu>
Date: Mon, 26 Sep 2005 15:05:26 +0000 (+0000)
Subject: *** empty log message ***
X-Git-Tag: LAST_BEFORE_NEW~1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;p=helm.git

*** empty log message ***
---

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 8ced53889..ed22ef472 100644
--- 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 197ceffbb..e8afa8032 100644
--- 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