diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-27 12:45:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-27 12:45:11 +0200 |
| commit | 4db867c45dafc7ed7b524a8d089cd57b7944feca (patch) | |
| tree | 8d0979ff8570308a56b8db43ec56637ea151e1f6 /pretyping/recordops.ml | |
| parent | f25ebf0a2d163df5191cf20650c82955b17972f7 (diff) | |
Add an init_setoid check in rewrite to avoid trying to get undefined references.
Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded.
Diffstat (limited to 'pretyping/recordops.ml')
0 files changed, 0 insertions, 0 deletions