diff options
| author | Pierre-Marie Pédrot | 2016-09-08 23:44:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-09 00:08:21 +0200 |
| commit | 5ecd8a6a5593d7f197a115b129ebd5f530e40161 (patch) | |
| tree | d2023cfab1224ebb6f8f8ffb2edf44eb5deb6802 /dev/doc | |
| parent | e65c629bac48e61b3a14f05bfafc6b85486359c0 (diff) | |
Fix bug #3920 for good after 44ada64.
The previous commit did not apply the beta reduction for compatibility on the
correct goal. We rather apply it on the first generated subgoal. This fixes the
ergo contrib.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions