From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 19 Jul 2005 13:25:36 +0000 (+0000)
Subject: message if the duplicate check may take too long
X-Git-Tag: V_0_7_2~167
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a744f0790c6483f0e962e7392b1f588ec10895d;p=helm.git

message if the duplicate check may take too long
---

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 ->