diff options
| author | Hugo Herbelin | 2017-02-02 17:55:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 12:17:35 +0100 |
| commit | c6d6e8e5eba5420304fb387430294926cb3fc136 (patch) | |
| tree | e628a86d0ec0c36c8cdc2b10582c130b11fe21fe /interp/implicit_quantifiers.ml | |
| parent | 8965549b994262a27f5dd204d9c4012501d1a040 (diff) | |
Type extended_glob_local_binder now contains only glob_constr.
No more constr_expr in it.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions