message if the duplicate check may take too long

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3d738e1b9b74e62f2c7f21155dc56a19a96263cc..a744ba925ee73bdd09ae0b5ba9de0c7db2328af0 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -627,6 +627,12 @@ let eval_command opts status cmd =
            begin
              let dbd = MatitaDb.instance () in
              let similar = MetadataQuery.match_term ~dbd ty in
+             let similar_len = List.length similar in
+             if similar_len> 30 then
+               (MatitaLog.message
+                 ("Duplicate check will compare your theorem with " ^ 
+                   string_of_int similar_len ^ 
+                   " theorems, this may take a while."));
              let convertible =
                List.filter (
                  fun u ->