From 28ac70d3f475442cda4ef30e0e9c0e6d012b2527 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 26 Sep 2005 15:05:26 +0000 Subject: [PATCH] *** empty log message *** --- helm/ocaml/paramodulation/indexing.ml | 5 +++-- helm/ocaml/paramodulation/saturation.ml | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) 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 -- 2.39.2