summaryrefslogtreecommitdiff
path: root/include/request.h
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-02 14:11:18 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-02 14:11:18 -0500
commit686b727ebba1749f1936cfc39a7b6b1f1f6ebc0a (patch)
tree9a7a5b5d9c691037e497e7f105a998d087ebfe47 /include/request.h
parent83f86225d56718fae1f226202efda9d69a5c369f (diff)
Instantiate any Unit unification variables that remain after elaboration
Diffstat (limited to 'include/request.h')
0 files changed, 0 insertions, 0 deletions