diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-21 22:23:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 00:44:26 +0200 |
| commit | ca630605330828b9b6456477b0fd4f8a0c3f1831 (patch) | |
| tree | e04712936c193bbe5daade5843f9f8eb5a8c38fc /interp/constrexpr_ops.ml | |
| parent | 09e15424aab082fd4b18a06e8894227beddeb487 (diff) | |
More precise on preventing clash between bound vars name and hidden impargs.
We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.
This fixes previous commit, with which it could possibly be merged.
Diffstat (limited to 'interp/constrexpr_ops.ml')
0 files changed, 0 insertions, 0 deletions