diff options
| author | Hugo Herbelin | 2015-12-14 15:04:52 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-01-14 14:36:10 +0100 |
| commit | 33617aa7b36f157f6314a83dde6ba45164ddd05b (patch) | |
| tree | fa412ff8488ac263b33e58392c5658226c3b0f82 /kernel/cbytecodes.ml | |
| parent | c7a7d55e0dc47a097bf0d0c8897bc490ce55577b (diff) | |
Changing "P is assumed" to "P is declared".
The term "assumed" refers more to the type of the object than to the
name of the object. It is particularly misguiding when P:Prop since P
is assumed would suggest that a proof of P is assumed, and not that
the variable P itself is declared (see discussion with P. Castéran on
coqdev: "Chapter 4 of the Reference Manual", 8/10/2015).
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions