aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/leminv.ml
AgeCommit message (Expand)Author
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias