aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
authorMatthieu Sozeau2017-07-31 16:49:06 +0200
committerMatthieu Sozeau2017-09-19 10:28:03 +0200
commit8966c9241207b6f5d4ee38508246ee97ed006e72 (patch)
tree774d61f09e653e084c9fc1c1b5fd01996ab09a76 /API
parentd9e54d65cc808eab2908beb7a7a2c96005118ace (diff)
proof_global: cleanup and comment close_proof
evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions