diff options
| author | Maxime Dénès | 2017-02-16 09:44:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-02-16 09:44:48 +0100 |
| commit | bcb634d070519d6e37d9b7d39f12437a7d38f0c2 (patch) | |
| tree | f14702bb8344d82c264966a95f1257d7184df4a7 /proofs | |
| parent | ec49fbd7fee9c6ff27f56498a6309d9651b4ef82 (diff) | |
| parent | 888d4be3ea2a45cff416fd8896276cfa8fc00518 (diff) | |
Merge PR#403: Split Vernacular Processing from Toplevel
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a2ee622215..120cde5e55 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -317,7 +317,10 @@ let constrain_variables init uctx = let cstrs = UState.constrain_variables levels uctx in Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) -let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context + +let close_proof ~keep_body_ucst_separate ?feedback_id ~now + (fpl : closed_proof_output Future.computation) = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in @@ -395,8 +398,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = universes = (universes, binders) }, fun pr_ending -> CEphemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context - let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin |