diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-18 19:38:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-25 10:59:24 +0100 |
| commit | df9d69f3ccf3e5600919a21112afda00b463fbc5 (patch) | |
| tree | 95bcb0f7e45ae7c6f3e9c1584f2551862ee947f2 /tactics/tactics.ml | |
| parent | c3e01a044297d322d8a5e6830fe3af002ebd2dce (diff) | |
Fixing a bug in the order of side conditions for introduction pattern -> and <-.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2e7adc513..0c4c5b673 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2240,7 +2240,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with | IntroInjection l' -> intro_decomp_eq loc l' thin tac id | IntroRewrite l2r -> - Tacticals.New.tclTHENLAST + Tacticals.New.tclTHENFIRST (* Skip the side conditions of the rewriting step *) (rewrite_hyp style l2r id) (tac thin None []) |