| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-19 | extensionality: Handle dependently-used hypotheses | Jason Gross | |
| 2016-09-19 | Adding an "extensionality in H" tactic which applies functional | Hugo Herbelin | |
| extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |