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