diff options
| author | Maxime Dénès | 2017-05-05 18:11:58 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-05 18:11:58 +0200 |
| commit | cd76a274c7d6fb71e109b6f3c87dd3a661f72e6c (patch) | |
| tree | 78b77f070e9afbc3257487234c973eb895cc21f4 /dev | |
| parent | a76a71eda10b054b04de4ff56f0637a32077edd4 (diff) | |
| parent | b4936da085b19ad508346d8e07ce1e922ef79c2d (diff) | |
Merge PR#558: Adding a fold_glob_constr_with_binders combinator
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions