diff options
author | 2017-07-28 18:25:30 +0200 | |
---|---|---|
committer | 2017-07-28 18:25:30 +0200 | |
commit | 17f37f42792b3150fcebb6236b9896845957b89d (patch) | |
tree | 5e76522bd7e5b16fe37907386f589a290078f0a0 /vernac/vernacinterp.ml | |
parent | e8bb8ea0da02b926e076cf04ea1c82c547a30ea2 (diff) | |
parent | df49e6b29fa9e8ac971c3e08f20ae6cb0f5b9889 (diff) |
Merge PR #923: [api] Fix base_include LTAC parts.
Diffstat (limited to 'vernac/vernacinterp.ml')
0 files changed, 0 insertions, 0 deletions