diff options
author | 2017-09-09 14:00:42 +0200 | |
---|---|---|
committer | 2017-09-19 10:28:03 +0200 | |
commit | cd29948855c2cbd3f4065170e41f8dbe625e1921 (patch) | |
tree | e747c92a12074f2d0753b902c5fe00261d0a0fe4 /vernac/indschemes.mli | |
parent | c2b881aae9c71a34199d2c66282512f2bdb19cf6 (diff) |
Don't lose names in UState.universe_context.
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
Diffstat (limited to 'vernac/indschemes.mli')
0 files changed, 0 insertions, 0 deletions