aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refine.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-30 23:08:19 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-03 20:05:57 +0200
commit9262f440e8d8b8559c5488b1333c023f7305d811 (patch)
treef09ec49bd38357d949876ca4e494fe22ff2b6a0c /proofs/refine.mli
parent267c880c5e8b73770316518a2a820e779c121fdb (diff)
Allowing to pass arbitrary data in internalization environments.
Diffstat (limited to 'proofs/refine.mli')
0 files changed, 0 insertions, 0 deletions