diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-29 17:08:13 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-29 17:08:13 +0000 |
| commit | 8c174eb4df242ba9bf6dd0922ebb6b19985decf9 (patch) | |
| tree | bd7a0040fe2e08c90f6492ba1aa8dd9c82e59d5e /plugins | |
| parent | ba09151f7b63d4081ef02ea33be4196711b5ee04 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/invfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0b04a572f..a0fcb538c 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 |