diff options
| author | Hugo Herbelin | 2017-05-01 19:44:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 01:58:11 +0200 |
| commit | 94126f45582b7f02a6c16284cdc627b7b0fe53ac (patch) | |
| tree | 0cb5eff7c80ae45ccf091e620a3ba4257a7fa389 /dev/include | |
| parent | a3407e27e60104fa8ea2e62433f9920a41a22757 (diff) | |
Factorizing interp_gen through a function interpreting glob_constr.
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions