diff options
| author | Pierre-Marie Pédrot | 2020-06-24 20:46:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-05 21:41:08 +0200 |
| commit | 5c1730ca2533b17066e7ee5c672ae6aa5fdef1dc (patch) | |
| tree | b987aace7f89582895c8b3e7017612c5530faf15 /pretyping/reductionops.ml | |
| parent | 69d25dedd34c70d1757e421023db89690114ff27 (diff) | |
Inline mutual recursion helpers in simpl implementation.
This highlights static invariants about the function.
Diffstat (limited to 'pretyping/reductionops.ml')
0 files changed, 0 insertions, 0 deletions