Start using strict bulleting everywhere
Set Default Goal Selector "!" makes it illegal to ever apply a tactic with more than one goal (instead, must focus with bullets or braces).
parent
d9bb5450
No related branches found
No related tags found
Showing
- theories/base.v 9 additions, 2 deletionstheories/base.v
- theories/decidable.v 1 addition, 1 deletiontheories/decidable.v
- theories/lexico.v 7 additions, 3 deletionstheories/lexico.v
- theories/list.v 48 additions, 30 deletionstheories/list.v
- theories/numbers.v 17 additions, 11 deletionstheories/numbers.v
- theories/orders.v 3 additions, 3 deletionstheories/orders.v
- theories/proof_irrel.v 1 addition, 1 deletiontheories/proof_irrel.v
- theories/sets.v 4 additions, 4 deletionstheories/sets.v
- theories/sorting.v 2 additions, 2 deletionstheories/sorting.v
- theories/vector.v 10 additions, 6 deletionstheories/vector.v
Loading
Please register or sign in to comment