| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-26 | Fixes #13456: regression where tactic exists started to check evars ↵ | Hugo Herbelin | |
| incrementally. The regression was due to #12365. We fix it by postponing the evars check after the calls to the underlying constructor tactic, while retaining using information from the first instantiations to resolve the latter instantiations. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |