diff options
Diffstat (limited to 'ltac/coretactics.ml4')
| -rw-r--r-- | ltac/coretactics.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index de4d589eee..6186667584 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -151,7 +151,10 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] -| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ] +END + +TACTIC EXTEND symmetry_in +| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) |