diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
commit | 3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch) | |
tree | 0dd3a804e1924862390a7f78abc9a8a119127f9c /proofs | |
parent | ceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff) | |
parent | 1bc1cba7a759a285131a3ed6ea8979716700b856 (diff) |
Merge remote-tracking branch 'github/pr/283' into trunk
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/pfedit.ml | 9 | ||||
-rw-r--r-- | proofs/pfedit.mli | 2 | ||||
-rw-r--r-- | proofs/proof_global.ml | 4 |
3 files changed, 9 insertions, 6 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 86c2b7a57..d55d6ce6b 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 diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index f2f4b11ed..aa01969b7 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -169,7 +169,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context 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 |