Merge features of version 2.1.1 into coq-master

impermeable / coq-waterproof

GNU Lesser General Public License v3.0

29 stars 9 forks source link

Closed jim-portegies closed 6 months ago

jim-portegies commented 6 months ago

Bring the features of version 2.1.1 that were developed against coq version 8.17 to coq-master:

Improve the Either tactic: now proves and destructs ordinary 'ors' when the goal is a proposition
Improve some mathematical definitions
Add vernacular for debugging automation
Add a tactic for strong induction