fixed a bug (status not reset properly between calls), tried some other

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index ac99340005eec05a88c3209c0b175168dcb8d6a8..0556c442df8146f7c6f50961dc44149f400d4a18 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1256,7 +1256,8 @@ let find_library_theorems dbd env status equalities_uris =
     in
     List.fold_left
       (fun s u -> UriManager.UriSet.add u s)
-      s [sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); eq_ind_r_URI ()]
+      s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
+         eq_ind_r_URI ()]
   in
   let metasenv, context, ugraph = env in
   let candidates =
@@ -1266,10 +1267,16 @@ let find_library_theorems dbd env status equalities_uris =
          else
            let t = CicUtil.term_of_uri uri in
            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
-           (t, ty, [])::l)
+           (uri, t, ty, [])::l)
       [] (MetadataQuery.signature_of_goal ~dbd status)
   in
-  candidates
+  let refl_equal =
+    let u = eq_XURI () in
+    let t = CicUtil.term_of_uri u in
+    let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+    (u, t, ty, [])
+  in
+  refl_equal::candidates
 ;;
 
 
@@ -1370,7 +1377,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
                      else
                        let _, context, ty = CicUtil.lookup_meta i menv in
                        (i, (context, Cic.Meta (j, l), ty))::s
-                   with Not_found ->
+                   with Not_found | CicUtil.Meta_not_found _ ->
 (*                      debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
                      s
                  )