diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-31 22:46:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-31 22:46:05 +0200 |
| commit | 6add354ad9ca0f68d3ef311c4e53ee96d9fdb4d7 (patch) | |
| tree | c4499365e809a58ce93d2af39ab8e2cfa3933c17 /kernel/term.mli | |
| parent | a20494163815e4b8275c4d0412d6c857c95263f4 (diff) | |
Ensuring proper cast invariants in EConstr.kind.
The kernel does fishy things with casts, such that ensuring there are no
two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr
view as well.
Diffstat (limited to 'kernel/term.mli')
0 files changed, 0 insertions, 0 deletions