diff options
| author | Emilio Jesus Gallego Arias | 2019-06-06 06:01:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:54:43 +0200 |
| commit | 70a11c78e790d7f2f4175d1002e08f79d3ed8486 (patch) | |
| tree | fc184b3b7d59b20e6e5f0c1a82a88c1b15fc45bb /proofs | |
| parent | fd2d2a8178d78e441fb3191cf112ed517dc791af (diff) | |
[proof] More uniformity in proof start labels.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 14 |
3 files changed, 10 insertions, 10 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 64d21be7e8..98002de119 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -119,7 +119,7 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof evd id ~poly UState.default_univ_decl goal_kind goals in + let pf = Proof_global.start_proof ~name:id ~poly ~udecl:UState.default_univ_decl ~kind:goal_kind evd goals in try let pf, status = by tac pf in let open Proof_global in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 22f818edbb..8ac4435539 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -94,7 +94,7 @@ let set_endline_tactic tac ps = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma name udecl ~poly kind goals = +let start_proof ~name ~udecl ~poly ~kind sigma goals = { proof = Proof.start ~name ~poly sigma goals ; endline_tactic = None ; section_vars = None @@ -102,7 +102,7 @@ let start_proof sigma name udecl ~poly kind goals = ; strength = kind } -let start_dependent_proof name udecl ~poly kind goals = +let start_dependent_proof ~name ~udecl ~poly ~kind goals = { proof = Proof.dependent_start ~name ~poly goals ; endline_tactic = None ; section_vars = None diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 5bfed948ba..2c328bcf12 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -63,21 +63,21 @@ type opacity_flag = Opaque | Transparent typically contain universe constraints), and with universe bindings pl. *) val start_proof - : Evd.evar_map - -> Names.Id.t - -> UState.universe_decl + : name:Names.Id.t + -> udecl:UState.universe_decl -> poly:bool - -> Decl_kinds.goal_kind + -> kind:Decl_kinds.goal_kind + -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof - : Names.Id.t - -> UState.universe_decl + : name:Names.Id.t + -> udecl:UState.universe_decl -> poly:bool - -> Decl_kinds.goal_kind + -> kind:Decl_kinds.goal_kind -> Proofview.telescope -> t |