-
Armaël Guéneau authored
It seems the hsimpl tactic was in some cases working thanks to a bug in Ltac pattern matching, introduced in Coq 8.4, and that was fixed in Coq 8.6.1 (https://github.com/coq/coq/issues/5487). The fix implemented here makes hsimpl slightly more powerful in some cases, so proofs may need to be updated.
1f74a730