diff options
| author | Arnaud Spiwack | 2014-07-22 17:15:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-23 17:42:36 +0200 |
| commit | 1fd8e23da73422b17209e2d69a19dca6789bcaed (patch) | |
| tree | 37c854c17adf96424ec95555b24c5e61033f98c2 /proofs/proof.ml | |
| parent | aa63497700bb2e75767c1891a961fc06ba329065 (diff) | |
Change the interface of proof_global to take an evar_map instead of a universe context to start proofs.
It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.
Diffstat (limited to 'proofs/proof.ml')
0 files changed, 0 insertions, 0 deletions