aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refine.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-24 09:56:55 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-29 14:07:34 +0100
commita41f8601655f69e71b621dba192342ed0e1f8ec2 (patch)
tree921861c20db73501b325befb8ce719f798abc30c /proofs/refine.ml
parentb23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff)
[proof] [api] Rename proof types in preparation for functionalization.
In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
Diffstat (limited to 'proofs/refine.ml')
0 files changed, 0 insertions, 0 deletions