diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 15:17:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 15:36:54 +0200 |
| commit | 85f95cc9f11dc630e59f3a13362e151134ce92ea (patch) | |
| tree | 69cf3cfab62a6186539a976c2c98bc823d45b296 /pretyping/indrec.ml | |
| parent | adbc03f4ec1fa8d21343fc252b1462b582665aeb (diff) | |
Really honor the [simpl never] flag in whd_simpl, it was still doing reductions in
case the constant was hiding a direct match for example. Also avoid two lookups
of ReductionBehavior per constant application in simpl.
Diffstat (limited to 'pretyping/indrec.ml')
0 files changed, 0 insertions, 0 deletions