From 0a744f0790c6483f0e962e7392b1f588ec10895d Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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