From 1847057e19e518fd8ab87ead5d7fdd006dfa0367 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Nov 2008 21:27:50 +0000
Subject: Adaptation to ocaml 3.11 new semantics of String.index_from (see bug
 #1974) Grant wish #1988 ("fun" forces reduction in "refine" if needed)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/refine.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/refine.ml b/tactics/refine.ml
index c0db5def58..9225fd9d7c 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -275,7 +275,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
     | Lambda (Name id,_,m), _ ->
 	assert (isMeta (strip_outer_cast m));
 	begin match sgp with
-	  | [None] -> introduction id gl
+	  | [None] -> intro_mustbe_force id gl
 	  | [Some th] ->
               tclTHEN (introduction id)
                 (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)) gl
-- 
cgit v1.2.3