diff options
author | 2018-03-09 13:09:16 +0100 | |
---|---|---|
committer | 2018-03-09 13:09:16 +0100 | |
commit | 0c345d64d67c01c7b7a75bf23391b421f95c4fb7 (patch) | |
tree | f86b9a5c1093dfe66f744c86f8ed8ab6bae993d6 /vernac/obligations.ml | |
parent | 16f93d201cf7e379d5acf533be20fed30bbc212c (diff) | |
parent | 17f9e85d9785b2ab77426e6d8644840fa7f37d85 (diff) |
Merge PR #6871: [build] Simpler byte/opt toplevel build.
Diffstat (limited to 'vernac/obligations.ml')
0 files changed, 0 insertions, 0 deletions