diff options
| author | Tanaka Akira | 2019-02-08 11:34:43 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-02-08 11:34:43 +0900 |
| commit | 613b9ee88067392b7681ee5f0c28d5c5cfff6276 (patch) | |
| tree | c5e42889cc25f205b2400cbd6128b6080f5be790 /kernel/type_errors.ml | |
| parent | ca40e534580a67ca327b5f1b054e4089ac2ee281 (diff) | |
Change c to c' forgotten at exchanging c and c'.
In Cic admissible rules section, c and c' are exchanged at
https://github.com/coq/coq/commit/8654b03544f0efe4b418a0afdc871ff84784ff83 .
But the exchange is not complete.
This commit complete it.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions