*** empty log message ***

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

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 =