diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 05:33:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:54:43 +0200 |
| commit | fd2d2a8178d78e441fb3191cf112ed517dc791af (patch) | |
| tree | 8a85d441d2a25ad1ee4f46ef498694be9e9a8a12 /proofs/proof_global.ml | |
| parent | fb92bcc7830a084a4a204c4f58c44e83c180a9c9 (diff) | |
[proof] Remove duplicated universe polymorphic from decl_kinds
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2f7e5d618a..22f818edbb 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -39,6 +39,7 @@ type 'a proof_entry = { type proof_object = { id : Names.Id.t ; entries : Evd.side_effects proof_entry list + ; poly : bool ; persistence : Decl_kinds.goal_kind ; universes: UState.t ; udecl : UState.universe_decl @@ -69,7 +70,8 @@ let map_fold_proof_endline f ps = | None -> Proofview.tclUNIT () | Some tac -> let open Geninterp in - let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in + let {Proof.poly} = Proof.data ps.proof in + let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in let tac = Geninterp.interp tag ist tac in Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) @@ -92,16 +94,16 @@ 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 kind goals = - { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals +let start_proof sigma name udecl ~poly kind goals = + { proof = Proof.start ~name ~poly sigma goals ; endline_tactic = None ; section_vars = None ; udecl ; strength = kind } -let start_dependent_proof name udecl kind goals = - { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals +let start_dependent_proof name udecl ~poly kind goals = + { proof = Proof.dependent_start ~name ~poly goals ; endline_tactic = None ; section_vars = None ; udecl @@ -254,7 +256,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now proof_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { id = name; entries = entries; persistence = strength; universes; udecl } + { id = name; entries = entries; poly; persistence = strength; universes; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in |