diff options
| author | Hugo Herbelin | 2017-05-19 21:19:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-19 21:25:59 +0200 |
| commit | 234dc568769602cb91655929a344027a15f52845 (patch) | |
| tree | f4d1a973c474d46612c84ac0c765a712fbe4dc65 /kernel/type_errors.ml | |
| parent | 6ceaf0176b2a61cd2ed7b358af1e34349a8041ce (diff) | |
In EConstr, defining some "cast" functions earlier.
This allows to use a cast in subst_of_rel_context_instance.
Also added more cast functions for further use.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions