From 109e85dee481b9a00e6c27648ea62fc4048b0208 Mon Sep 17 00:00:00 2001
From: jforest
Date: Tue, 27 Nov 2007 23:10:50 +0000
Subject: bug correction in functional inversion principle generation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10340 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/invfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index b975c2e937..6171e81948 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -569,14 +569,14 @@ let rec reflexivity_with_destruct_cases g =
 		     if Equality.discriminable (pf_env g) (project g) t1 t2 
 		     then Equality.discr id g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHEN (Equality.inj [] id) intros_with_rewrite  g
+		     then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
   in
   (tclFIRST
     [ reflexivity;
-      destruct_case ();
+      tclTHEN (tclPROGRESS discr_inject) (destruct_case ());
       (*  We reach this point ONLY if 
 	  the same value is matched (at least) two times 
 	  along binding path.
-- 
cgit v1.2.3