diff options
| author | Hugo Herbelin | 2014-06-26 14:23:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-26 14:50:12 +0200 |
| commit | 55e46598fac67157a5b2c820be621d254581b888 (patch) | |
| tree | 61db2f9a76b3bb55c5fc0131be9600227efc31c2 /kernel/type_errors.ml | |
| parent | 68d60b7c33b11ad452eca3d2a7ec320963064a9d (diff) | |
Deactivate the "Standard Propositions Naming" flag, source of a lot of
incompatibilities, at least until the check of compilation of contribs
succeeds more often.
Incidentally adapted some proofs in Reals which were not agnostic
relatively to whether the option is on or off.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions