diff options
| author | Maxime Dénès | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /proofs/pfedit.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/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 86c2b7a573..d55d6ce6ba 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -147,7 +147,10 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = +let default_goal_kind = + { locality = Global; polymorphic = false; object_kind = Proof Theorem } + +let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ tac = let evd = Evd.from_ctx ctx in let terminator = Proof_global.make_terminator (fun _ -> ()) in start_proof id goal_kind evd sign typ terminator; @@ -161,10 +164,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env ctx ?(polymorphic=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let gk = Global, poly, Proof Theorem in + let gk = { locality = Global; polymorphic; object_kind = Proof Theorem } in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce |