diff options
| author | Hugo Herbelin | 2017-02-02 17:10:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 12:17:35 +0100 |
| commit | 8965549b994262a27f5dd204d9c4012501d1a040 (patch) | |
| tree | 5bc257b9aa36f9b4be0e9c8788cdbd526508db60 /dev/include | |
| parent | a1e5a87c9d4368fe17d93988b010acfb1c96771b (diff) | |
Standardized the order of constructors for binders: Assum then Def.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions