diff options
| author | Gaëtan Gilbert | 2018-09-27 15:35:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-28 16:09:40 +0200 |
| commit | bc26ad1cbbeb0a8aa2ac36916db3c09330bacfd0 (patch) | |
| tree | bf40b3f59d7610397de120e052eab1d734f0f591 /engine/eConstr.ml | |
| parent | d0122151acdbe15b88d144b730baf5b0febf3c70 (diff) | |
Generalize type of compare_head_with functions
Diffstat (limited to 'engine/eConstr.ml')
0 files changed, 0 insertions, 0 deletions