diff options
| author | Arnaud Spiwack | 2014-12-04 09:21:30 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-04 14:38:05 +0100 |
| commit | f66b84de608830600e43f6d1a97c29226b6b58ea (patch) | |
| tree | e8a4ecad63a04ee1462487aeafa58b301335b713 /dev/include | |
| parent | 446b9c571c29f740475e39c19c4037b8102f1f21 (diff) | |
Refine primitive: [unsafe] is now true by default.
Generally, tactics build type-correct terms. A safe refine is hence a waste of time (somtimes a significant one). The safe option is kept for specific purposes such as debugging, or some weird interaction with the pretyper and universes which still seemed to hold last time I checked (used by the user-level refine tactic).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions