added a new type for proofs.

[helm.git] / helm / software / components / tactics / autoTactic.ml

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 42df90768263b2749c30f9ff81c1c0dcf4f9b12c..9db6ed1c9094d3816c374592d401d5ba35fcdd7f 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -334,7 +334,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
       | Some _ ->
           let _, metasenv, _, _ = proof in
           let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          full || (Inference.term_is_equality meta_goal)
+          full || (Equality.term_is_equality meta_goal)
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");