X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;fp=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=ed22ef4721745369614be57fc2b65274bea0027f;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;hp=8ced5388922fe31e384c80a9efa5ec5860a487c9;hpb=9547c888a55a5372ff2f6a2d2a9eab7d5d7c01fb;p=helm.git

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 =