diff options
Diffstat (limited to 'theories/MSets/MSetGenTree.v')
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 704ff31be..cacd91343 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -378,7 +378,7 @@ Ltac invtree f := Ltac inv := inv_ok; invtree InT. -Ltac intuition_in := repeat progress (intuition; inv). +Ltac intuition_in := repeat (intuition; inv). (** Helper tactic concerning order of elements. *) |