aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-19 21:19:51 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-19 21:25:59 +0200
commit234dc568769602cb91655929a344027a15f52845 (patch)
treef4d1a973c474d46612c84ac0c765a712fbe4dc65 /lib/feedback.mli
parent6ceaf0176b2a61cd2ed7b358af1e34349a8041ce (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 'lib/feedback.mli')
0 files changed, 0 insertions, 0 deletions