diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /proofs/proof_global.ml | |
| parent | 424de98770e1fd8c307a7cd0053c268a48532463 (diff) | |
Stylistic improvements in intf/decl_kinds.mli.
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2956d623f..911d4ffbc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -320,7 +320,7 @@ let constrain_variables init uctx = let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in - let poly = pi2 strength (* Polymorphic *) in + let poly = strength.Decl_kinds.polymorphic in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in @@ -398,7 +398,7 @@ 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 return_proof ?(allow_partial=false) () = - let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + let { pid; proof; strength = { Decl_kinds.polymorphic }} = cur_pstate () in if allow_partial then begin let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in |