diff options
| author | Hugo Herbelin | 2015-10-11 14:36:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-11 15:21:33 +0200 |
| commit | e9995f6e9f9523d4738d9ee494703b6f96bf995d (patch) | |
| tree | ce5297379247c6af9e6c16ba45b5b7e479b96d3c /kernel | |
| parent | ae5305a4837cce3c7fd61b92ce8110ac66ec2750 (diff) | |
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions