diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-23 18:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-23 18:25:15 +0200 |
| commit | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (patch) | |
| tree | 7546ab8a3bf1a0e2b5a75028e9efcade1d8d4321 /library/heads.mli | |
| parent | 13716dc6561a3379ba130f07ce7ecd1df379475c (diff) | |
Hopefully better names to constructors of internal_flag, as discussed
with Enrico.
Diffstat (limited to 'library/heads.mli')
0 files changed, 0 insertions, 0 deletions