From 8c174eb4df242ba9bf6dd0922ebb6b19985decf9 Mon Sep 17 00:00:00 2001
From: jforest
Date: Wed, 29 Feb 2012 17:08:13 +0000
Subject: correcting a little bug in invfun.ml

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

(limited to 'plugins')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0b04a572fe..a0fcb538c8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -588,15 +588,15 @@ let rec reflexivity_with_destruct_cases g =
     )
   in
   (tclFIRST
-    [ reflexivity;
-      tclTHEN (tclPROGRESS discr_inject) (destruct_case ());
+    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity;
+      observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
       (*  We reach this point ONLY if
 	  the same value is matched (at least) two times
 	  along binding path.
 	  In this case, either we have a discriminable hypothesis and we are done,
 	  either at least an injectable one and we do the injection before continuing
       *)
-      tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases
+      observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases)
     ])
     g
 
-- 
cgit v1.2.3