diff options
| author | Pierre-Marie Pédrot | 2014-12-02 18:29:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-12-02 18:48:40 +0100 |
| commit | 801c1c288e1a82a6eeacf7518b2a2a53f4d09c75 (patch) | |
| tree | 29c24000eebff877eebd4da2ecc20efe52f507c2 /dev/include | |
| parent | ae9f7011a8441a3e34c9fc98497c0e663fb877ca (diff) | |
For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota
normalize it afterwards.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions