diff options
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 14 |
2 files changed, 15 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2e7adc513a..0c4c5b673b 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 []) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 11156aa0ee..69d66f1008 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -84,3 +84,17 @@ Qed. Goal forall x : nat, True. intros y%(fun x => x). Abort. + +(* Fixing a bug in the order of side conditions of a "->" step *) + +Goal (True -> 1=0) -> 1=1. +intros ->. +- reflexivity. +- exact I. +Qed. + +Goal forall x, (True -> x=0) -> 0=x. +intros x ->. +- reflexivity. +- exact I. +Qed. |