| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-07 | [abbreviation] allow the user to set arguments scope | Enrico Tassi | |
| 2018-10-31 | Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes). | Hugo Herbelin | |
| We compute the binding to tactic-in-term once for all in the right scopes before interpreting the tactic. An alternative would have been to surround the constr_expr by CDelimiters to simulate its interpretation in the expected scopes (though this would not have worked for temporary scopes). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |