add a function to obtain a set with all elements of a finite type

See merge request iris/stdpp!196

add dom_insert_lookup

See merge request iris/stdpp!195

Remove dead type classes and notations.

See merge request iris/stdpp!197

These were very specific, there were no lemmas about them. They were used
back in the days for some specific things in my C semantics.

Add map_fmap_union for FinMap

See merge request iris/stdpp!194

Avoid relying on implicit instance generalization, and name some instances.

See merge request iris/stdpp!193

Fix in preparation for https://github.com/coq/coq/pull/13188

Drop support for Coq 8.8 and 8.9

See merge request !190

update Makefile

See merge request iris/stdpp!191

Add Qp lemmas

See merge request iris/stdpp!187

Thanks to @simongregersen for reporting.

Note that prior to 0d7a7f06 we would get this instance automatically,
but that instance would not have the right computational behavior.

add version of Qp_lower_bound that returns less-than facts

See merge request iris/stdpp!186

Add "options" file

Closes #81

See merge request iris/stdpp!185

Switch to strict bulleting everywhere

See merge request iris/stdpp!184

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).