aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmlambda.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-11-14 16:14:48 +0100
committerHugo Herbelin2020-11-24 15:29:16 +0100
commit47910007a9eff37c9f364a269b46874165711abf (patch)
tree6d9a6cc4b77840ea045e6c5d68d7c5c1cd152484 /kernel/vmlambda.ml
parent90cb2b0daf54cbd72c5ac8e1ffe2007c8901ddba (diff)
Add a new evar source to refer to evars which are types of evars.
To tie the knot (since the evar depends on the evar type and the source of the evar type of the evar), we use an "update_source" function. An alternative could be to provide a function to build both an evar with its evar type directly in evd.ml...
Diffstat (limited to 'kernel/vmlambda.ml')
0 files changed, 0 insertions, 0 deletions