diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 01:38:39 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 17:45:55 +0100 |
commit | 53f5cc210da4debd5264d6d8651a76281b0b4256 (patch) | |
tree | 8e1edbb93c15a88480c8bc4454cc9b8fc15c88c1 /vernac/vernacentries.ml | |
parent | c75619228e1c878644edbc49c5cb690777966863 (diff) |
[econstr] Switch constrintern API to non-imperative style.
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions