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

See merge request !196

add dom_insert_lookup

See merge request !195

Remove dead type classes and notations.

See merge request !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 !194

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

See merge request !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 !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 !186

Add "options" file

Closes #81

See merge request !185

Switch to strict bulleting everywhere

See merge request !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).