Merge branch 'fix-hint-locality' into 'master'
Add explicit Global to hints at top level See merge request iris/stdpp!202
Showing
- theories/base.v 64 additions, 64 deletionstheories/base.v
- theories/coPset.v 2 additions, 2 deletionstheories/coPset.v
- theories/countable.v 1 addition, 1 deletiontheories/countable.v
- theories/decidable.v 2 additions, 2 deletionstheories/decidable.v
- theories/fin_maps.v 26 additions, 26 deletionstheories/fin_maps.v
- theories/finite.v 2 additions, 2 deletionstheories/finite.v
- theories/gmultiset.v 1 addition, 1 deletiontheories/gmultiset.v
- theories/list.v 4 additions, 4 deletionstheories/list.v
- theories/namespaces.v 10 additions, 10 deletionstheories/namespaces.v
- theories/nat_cancel.v 3 additions, 3 deletionstheories/nat_cancel.v
- theories/numbers.v 10 additions, 10 deletionstheories/numbers.v
- theories/option.v 2 additions, 2 deletionstheories/option.v
- theories/pretty.v 1 addition, 1 deletiontheories/pretty.v
- theories/proof_irrel.v 1 addition, 1 deletiontheories/proof_irrel.v
- theories/relations.v 1 addition, 1 deletiontheories/relations.v
- theories/sets.v 13 additions, 13 deletionstheories/sets.v
- theories/tactics.v 5 additions, 5 deletionstheories/tactics.v
- theories/telescopes.v 2 additions, 2 deletionstheories/telescopes.v
Loading
Please register or sign in to comment