From b683d0f2f60df91276a7a1c53660c01097d4e5c0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 20 Apr 2011 10:27:32 +0000
Subject: Don't force progress on instance applications, there is always
 progress when refining dependent instances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14031 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 356752480f..41894ec511 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -104,12 +104,12 @@ END
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
-    tclPROGRESS (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
+    Clenvtac.clenv_refine true ~with_classes:false clenv' gls
 
 let unify_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
-    tclPROGRESS (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
+    Clenvtac.clenv_refine false ~with_classes:false clenv' gls
 
 let clenv_of_prods nprods (c, clenv) gls =
   if nprods = 0 then Some clenv
-- 
cgit v1.2.3