From 0a744f0790c6483f0e962e7392b1f588ec10895d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 19 Jul 2005 13:25:36 +0000
Subject: [PATCH] message if the duplicate check may take too long

---
 helm/matita/matitaEngine.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3d738e1b9..a744ba925 100644
--- 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 ->
-- 
2.39.2